tuned exception handling;

--- 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}) =