Lines Matching defs:ERROR
15 val ERROR = mk_HOL_ERR "Parse";
30 val dest_forall = sdest_binder ("!","bool") (ERROR "dest_forall" "");
38 fun lhs tm = #2(sdest_binop("=","min") (ERROR"lhs" "") tm);
468 | _ => raise ERROR"typedTerm" "badly formed quotation")
507 | NONE => raise ERROR "grammar_typed_parse_in_context" "No consistent parse"
515 | NONE => raise ERROR "typed_parse_in_context" "No consistent parse"
689 end handle GrammarError s => raise ERROR "add_rule" ("Grammar error: "^s)
835 raise ERROR "temp_overload_on_by_nametype"
869 raise ERROR f "field selection term must be of type t -> a"
882 val err = ERROR f "fupdate term must be of type (a -> a) -> t -> t"
898 raise ERROR "add_numeral_form"
907 [] => raise ERROR "add_numeral_form" ("No constant with name "^s)
950 raise ERROR "update_overload_maps" ("Overload: "^s)
1126 [] => raise ERROR "merge_grammars" "Empty grammar list"