tuned exception handling;
authorwenzelm
Sat Jul 08 12:54:45 2006 +0200 (2006-07-08)
changeset 20057058e913bac71
parent 20056 0698a403a066
child 20058 7d035e26e5f9
tuned exception handling;
src/Pure/meta_simplifier.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sat Jul 08 12:54:44 2006 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sat Jul 08 12:54:45 2006 +0200
     1.3 @@ -553,7 +553,7 @@
     1.4        val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
     1.5          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     1.6      (*val lhs = Envir.eta_contract lhs;*)
     1.7 -      val a = the (cong_name (head_of (term_of lhs))) handle Option =>
     1.8 +      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
     1.9          raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    1.10        val (alist, weak) = congs;
    1.11        val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
    1.12 @@ -567,7 +567,7 @@
    1.13        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
    1.14          raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.15      (*val lhs = Envir.eta_contract lhs;*)
    1.16 -      val a = the (cong_name (head_of lhs)) handle Option =>
    1.17 +      val a = the (cong_name (head_of lhs)) handle Option.Option =>
    1.18          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    1.19        val (alist, _) = congs;
    1.20        val alist2 = List.filter (fn (x, _) => x <> a) alist;
    1.21 @@ -1020,8 +1020,7 @@
    1.22                                  NONE => thm
    1.23                                | SOME thm' => transitive3 thm
    1.24                                    (combination thm' (reflexive cr))
    1.25 -                           end handle TERM _ => error "congc result"
    1.26 -                                    | Pattern.MATCH => appc ()))
    1.27 +                           end handle Pattern.MATCH => appc ()))
    1.28                    | _ => appc ()
    1.29                 end)
    1.30           | _ => NONE)
    1.31 @@ -1170,7 +1169,7 @@
    1.32      val _ = check_bounds ss ct;
    1.33      val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct
    1.34    in dec simp_depth; res end
    1.35 -  handle exn => (dec simp_depth; raise exn);
    1.36 +  handle exn => (dec simp_depth; raise exn);  (* FIXME avoid handling of generic exceptions *)
    1.37  
    1.38  (*Rewrite a cterm*)
    1.39  fun rewrite_aux _ _ [] ct = Thm.reflexive ct
     2.1 --- a/src/Pure/pure_thy.ML	Sat Jul 08 12:54:44 2006 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Sat Jul 08 12:54:45 2006 +0200
     2.3 @@ -419,7 +419,8 @@
     2.4        fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
     2.5    | smart_store name_thm (name, thms) =
     2.6        let
     2.7 -        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th);
     2.8 +        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th)
     2.9 +          handle TERM (msg, _) => raise THM (msg, 0, [th]);
    2.10          val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
    2.11        in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
    2.12  
     3.1 --- a/src/Pure/thm.ML	Sat Jul 08 12:54:44 2006 +0200
     3.2 +++ b/src/Pure/thm.ML	Sat Jul 08 12:54:45 2006 +0200
     3.3 @@ -244,8 +244,8 @@
     3.4      val sorts = may_insert_term_sorts thy t [];
     3.5    in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
     3.6  
     3.7 -fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
     3.8 -  Theory.merge_refs (r1, r2);
     3.9 +fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
    3.10 +  Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise TERM (msg, [t1, t2]);
    3.11  
    3.12  (*Destruct application in cterms*)
    3.13  fun dest_comb (Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) =