--- a/src/Pure/meta_simplifier.ML Sat Jul 08 12:54:44 2006 +0200
+++ b/src/Pure/meta_simplifier.ML Sat Jul 08 12:54:45 2006 +0200
@@ -553,7 +553,7 @@
val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
(*val lhs = Envir.eta_contract lhs;*)
- val a = the (cong_name (head_of (term_of lhs))) handle Option =>
+ val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
val (alist, weak) = congs;
val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
@@ -567,7 +567,7 @@
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
raise SIMPLIFIER ("Congruence not a meta-equality", thm);
(*val lhs = Envir.eta_contract lhs;*)
- val a = the (cong_name (head_of lhs)) handle Option =>
+ val a = the (cong_name (head_of lhs)) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant", thm);
val (alist, _) = congs;
val alist2 = List.filter (fn (x, _) => x <> a) alist;
@@ -1020,8 +1020,7 @@
NONE => thm
| SOME thm' => transitive3 thm
(combination thm' (reflexive cr))
- end handle TERM _ => error "congc result"
- | Pattern.MATCH => appc ()))
+ end handle Pattern.MATCH => appc ()))
| _ => appc ()
end)
| _ => NONE)
@@ -1170,7 +1169,7 @@
val _ = check_bounds ss ct;
val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct
in dec simp_depth; res end
- handle exn => (dec simp_depth; raise exn);
+ handle exn => (dec simp_depth; raise exn); (* FIXME avoid handling of generic exceptions *)
(*Rewrite a cterm*)
fun rewrite_aux _ _ [] ct = Thm.reflexive ct
--- a/src/Pure/pure_thy.ML Sat Jul 08 12:54:44 2006 +0200
+++ b/src/Pure/pure_thy.ML Sat Jul 08 12:54:45 2006 +0200
@@ -419,7 +419,8 @@
fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
| smart_store name_thm (name, thms) =
let
- fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th);
+ fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th)
+ handle TERM (msg, _) => raise THM (msg, 0, [th]);
val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
--- a/src/Pure/thm.ML Sat Jul 08 12:54:44 2006 +0200
+++ b/src/Pure/thm.ML Sat Jul 08 12:54:45 2006 +0200
@@ -244,8 +244,8 @@
val sorts = may_insert_term_sorts thy t [];
in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
-fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
- Theory.merge_refs (r1, r2);
+fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
+ Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise TERM (msg, [t1, t2]);
(*Destruct application in cterms*)
fun dest_comb (Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =