sane ERROR handling;
authorwenzelm
Sat Jan 14 17:14:06 2006 +0100 (2006-01-14)
changeset 18678dd0c569fa43d
parent 18677 01265301db7f
child 18679 cf9f1584431a
sane ERROR handling;
TFL/casesplit.ML
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
src/CTT/ex/elim.ML
src/FOL/ex/IffOracle.thy
src/FOL/ex/foundn.ML
src/FOL/ex/int.ML
src/FOL/ex/quant.ML
src/FOLP/ex/foundn.ML
src/FOLP/ex/int.ML
src/FOLP/ex/quant.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_solver.ML
src/HOL/Tools/typedef_package.ML
src/HOL/ex/ROOT.ML
src/HOLCF/adm_tac.ML
src/HOLCF/cont_consts.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/pcpodef_package.ML
src/Provers/induct_method.ML
src/Pure/General/file.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_history.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_info.ML
src/Pure/axclass.ML
src/Pure/context.ML
src/Pure/goal.ML
src/Pure/old_goals.ML
src/Pure/proof_general.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Sequents/LK/quant.ML
src/ZF/Datatype.ML
src/ZF/Tools/ind_cases.ML
src/ZF/arith_data.ML
     1.1 --- a/TFL/casesplit.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/TFL/casesplit.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -100,13 +100,11 @@
     1.4        val dtypestab = DatatypePackage.get_datatypes sgn;
     1.5        val ty_str = case ty of
     1.6                       Type(ty_str, _) => ty_str
     1.7 -                   | TFree(s,_)  => raise ERROR_MESSAGE
     1.8 -                                            ("Free type: " ^ s)
     1.9 -                   | TVar((s,i),_) => raise ERROR_MESSAGE
    1.10 -                                            ("Free variable: " ^ s)
    1.11 +                   | TFree(s,_)  => error ("Free type: " ^ s)
    1.12 +                   | TVar((s,i),_) => error ("Free variable: " ^ s)
    1.13        val dt = case Symtab.lookup dtypestab ty_str
    1.14                  of SOME dt => dt
    1.15 -                 | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str)
    1.16 +                 | NONE => error ("Not a Datatype: " ^ ty_str)
    1.17      in
    1.18        cases_thm_of_induct_thm (#induction dt)
    1.19      end;
    1.20 @@ -138,7 +136,7 @@
    1.21              (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
    1.22              (Pv, Dv,
    1.23               Sign.typ_match sgn (Dty, ty) Vartab.empty)
    1.24 -          | _ => raise ERROR_MESSAGE ("not a valid case thm");
    1.25 +          | _ => error "not a valid case thm";
    1.26        val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
    1.27          (Vartab.dest type_insts);
    1.28        val cPv = ctermify (Envir.subst_TVars type_insts Pv);
    1.29 @@ -187,7 +185,7 @@
    1.30            end;
    1.31        val (n,ty) = case Library.get_first getter freets
    1.32                  of SOME (n, ty) => (n, ty)
    1.33 -                 | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr);
    1.34 +                 | _ => error ("no such variable " ^ vstr);
    1.35        val sgn = Thm.sign_of_thm th;
    1.36  
    1.37        val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
    1.38 @@ -284,7 +282,7 @@
    1.39               (writeln "th:";
    1.40                Display.print_thm th; writeln "split ths:";
    1.41                Display.print_thms splitths; writeln "\n--";
    1.42 -              raise ERROR_MESSAGE "splitto: cannot find variable to split on")
    1.43 +              error "splitto: cannot find variable to split on")
    1.44              | SOME v =>
    1.45               let
    1.46                 val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
    1.47 @@ -321,7 +319,7 @@
    1.48      fun add_eq (i, e) xs =
    1.49        (e, (get_related_thms i rules), i) :: xs
    1.50      fun solve_eq (th, [], i) =
    1.51 -          raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    1.52 +          error "derive_init_eqs: missing rules"
    1.53        | solve_eq (th, [a], i) = (a, i)
    1.54        | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
    1.55      val eqths =
     2.1 --- a/TFL/post.ML	Fri Jan 13 17:39:41 2006 +0100
     2.2 +++ b/TFL/post.ML	Sat Jan 14 17:14:06 2006 +0100
     2.3 @@ -207,7 +207,7 @@
     2.4        List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
     2.5  
     2.6    fun solve_eq (th, [], i) = 
     2.7 -      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
     2.8 +        error "derive_init_eqs: missing rules"
     2.9      | solve_eq (th, [a], i) = [(a, i)]
    2.10      | solve_eq (th, splitths as (_ :: _), i) = 
    2.11        (writeln "Proving unsplit equation...";
    2.12 @@ -215,7 +215,7 @@
    2.13            (CaseSplit.splitto splitths th), i)])
    2.14        (* if there's an error, pretend nothing happened with this definition 
    2.15           We should probably print something out so that the user knows...? *)
    2.16 -      handle ERROR_MESSAGE s => 
    2.17 +      handle ERROR s => 
    2.18               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
    2.19  in
    2.20  fun derive_init_eqs sgn rules eqs = 
     3.1 --- a/TFL/rules.ML	Fri Jan 13 17:39:41 2006 +0100
     3.2 +++ b/TFL/rules.ML	Sat Jan 14 17:14:06 2006 +0100
     3.3 @@ -819,7 +819,7 @@
     3.4      val result =
     3.5        if strict then Goal.prove thy [] [] t (K tac)
     3.6        else Goal.prove thy [] [] t (K tac)
     3.7 -        handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
     3.8 +        handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
     3.9    in #1 (freeze_thaw (standard result)) end;
    3.10  
    3.11  end;
     4.1 --- a/TFL/tfl.ML	Fri Jan 13 17:39:41 2006 +0100
     4.2 +++ b/TFL/tfl.ML	Sat Jan 14 17:14:06 2006 +0100
     4.3 @@ -578,7 +578,7 @@
     4.4       val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
     4.5                         theory Hilbert_Choice*)
     4.6           thm "Hilbert_Choice.tfl_some"
     4.7 -         handle ERROR => error
     4.8 +         handle ERROR msg => cat_error msg
     4.9      "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
    4.10       val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
    4.11   in {theory = theory, R=R1, SV=SV,
     5.1 --- a/src/CTT/ex/elim.ML	Fri Jan 13 17:39:41 2006 +0100
     5.2 +++ b/src/CTT/ex/elim.ML	Sat Jan 14 17:14:06 2006 +0100
     5.3 @@ -20,7 +20,7 @@
     5.4  result();
     5.5  writeln"first solution is fst;  backtracking gives snd";
     5.6  back(); 
     5.7 -back() handle ERROR => writeln"And there are indeed no others";  
     5.8 +back() handle ERROR _ => writeln"And there are indeed no others";  
     5.9  
    5.10  
    5.11  writeln"Double negation of the Excluded Middle";
     6.1 --- a/src/FOL/ex/IffOracle.thy	Fri Jan 13 17:39:41 2006 +0100
     6.2 +++ b/src/FOL/ex/IffOracle.thy	Sat Jan 14 17:14:06 2006 +0100
     6.3 @@ -40,12 +40,12 @@
     6.4  text {* These oracle calls had better fail *}
     6.5  
     6.6  ML {*
     6.7 -  (iff_oracle (the_context ()) 5; raise ERROR)
     6.8 +  (iff_oracle (the_context ()) 5; error "?")
     6.9      handle Fail _ => warning "Oracle failed, as expected"
    6.10  *}
    6.11  
    6.12  ML {*
    6.13 -  (iff_oracle (the_context ()) 1; raise ERROR)
    6.14 +  (iff_oracle (the_context ()) 1; error "?")
    6.15      handle Fail _ => warning "Oracle failed, as expected"
    6.16  *}
    6.17  
     7.1 --- a/src/FOL/ex/foundn.ML	Fri Jan 13 17:39:41 2006 +0100
     7.2 +++ b/src/FOL/ex/foundn.ML	Sat Jan 14 17:14:06 2006 +0100
     7.3 @@ -92,7 +92,7 @@
     7.4  goal IFOL.thy "EX y. ALL x. x=y";
     7.5  by (rtac exI 1);
     7.6  by (rtac allI 1);
     7.7 -by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
     7.8 +by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
     7.9  getgoal 1; 
    7.10  
    7.11  
     8.1 --- a/src/FOL/ex/int.ML	Fri Jan 13 17:39:41 2006 +0100
     8.2 +++ b/src/FOL/ex/int.ML	Sat Jan 14 17:14:06 2006 +0100
     8.3 @@ -84,12 +84,12 @@
     8.4  
     8.5  (*The attempt to prove them terminates quickly!*)
     8.6  Goal "((P-->Q) --> P)  -->  P";
     8.7 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
     8.8 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
     8.9  (*Check that subgoals remain: proof failed.*)
    8.10  getgoal 1;  
    8.11  
    8.12  Goal "(P&Q-->R)  -->  (P-->R) | (Q-->R)";
    8.13 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.14 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.15  getgoal 1;  
    8.16  
    8.17  
    8.18 @@ -272,24 +272,24 @@
    8.19  (*The attempt to prove them terminates quickly!*)
    8.20  
    8.21  Goal "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
    8.22 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.23 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.24  getgoal 1; 
    8.25  
    8.26  Goal "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
    8.27 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.28 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.29  getgoal 1; 
    8.30  
    8.31  Goal "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
    8.32 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.33 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.34  getgoal 1; 
    8.35  
    8.36  Goal "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
    8.37 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.38 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.39  getgoal 1; 
    8.40  
    8.41  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
    8.42  Goal "EX x. Q(x) --> (ALL x. Q(x))";
    8.43 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    8.44 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    8.45  getgoal 1; 
    8.46  
    8.47  
     9.1 --- a/src/FOL/ex/quant.ML	Fri Jan 13 17:39:41 2006 +0100
     9.2 +++ b/src/FOL/ex/quant.ML	Sat Jan 14 17:14:06 2006 +0100
     9.3 @@ -62,22 +62,22 @@
     9.4  writeln"The following should fail, as they are false!";
     9.5  
     9.6  Goal "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
     9.7 -by tac handle ERROR => writeln"Failed, as expected";  
     9.8 +by tac handle ERROR _ => writeln"Failed, as expected";  
     9.9  (*Check that subgoals remain: proof failed.*)
    9.10  getgoal 1; 
    9.11  
    9.12  Goal "(EX x. Q(x))  -->  (ALL x. Q(x))";
    9.13 -by tac handle ERROR => writeln"Failed, as expected";  
    9.14 +by tac handle ERROR _ => writeln"Failed, as expected";  
    9.15  getgoal 1; 
    9.16  
    9.17  Goal "P(?a) --> (ALL x. P(x))";
    9.18 -by tac handle ERROR => writeln"Failed, as expected";
    9.19 +by tac handle ERROR _ => writeln"Failed, as expected";
    9.20  (*Check that subgoals remain: proof failed.*)
    9.21  getgoal 1;  
    9.22  
    9.23  Goal
    9.24      "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
    9.25 -by tac handle ERROR => writeln"Failed, as expected";
    9.26 +by tac handle ERROR _ => writeln"Failed, as expected";
    9.27  getgoal 1;  
    9.28  
    9.29  
    10.1 --- a/src/FOLP/ex/foundn.ML	Fri Jan 13 17:39:41 2006 +0100
    10.2 +++ b/src/FOLP/ex/foundn.ML	Sat Jan 14 17:14:06 2006 +0100
    10.3 @@ -92,7 +92,7 @@
    10.4  goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
    10.5  by (rtac exI 1);
    10.6  by (rtac allI 1);
    10.7 -by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
    10.8 +by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
    10.9  getgoal 1; 
   10.10  
   10.11  
    11.1 --- a/src/FOLP/ex/int.ML	Fri Jan 13 17:39:41 2006 +0100
    11.2 +++ b/src/FOLP/ex/int.ML	Sat Jan 14 17:14:06 2006 +0100
    11.3 @@ -63,12 +63,12 @@
    11.4  
    11.5  (*The attempt to prove them terminates quickly!*)
    11.6  goal (theory "IFOLP") "?p : ((P-->Q) --> P)  -->  P";
    11.7 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    11.8 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
    11.9  (*Check that subgoals remain: proof failed.*)
   11.10  getgoal 1;  
   11.11  
   11.12  goal (theory "IFOLP") "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
   11.13 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.14 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.15  getgoal 1;  
   11.16  
   11.17  
   11.18 @@ -205,24 +205,24 @@
   11.19  (*The attempt to prove them terminates quickly!*)
   11.20  
   11.21  goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
   11.22 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.23 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.24  getgoal 1; 
   11.25  
   11.26  goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
   11.27 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.28 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.29  getgoal 1; 
   11.30  
   11.31  goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
   11.32 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.33 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.34  getgoal 1; 
   11.35  
   11.36  goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
   11.37 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.38 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.39  getgoal 1; 
   11.40  
   11.41  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
   11.42  goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
   11.43 -by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   11.44 +by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   11.45  getgoal 1; 
   11.46  
   11.47  
    12.1 --- a/src/FOLP/ex/quant.ML	Fri Jan 13 17:39:41 2006 +0100
    12.2 +++ b/src/FOLP/ex/quant.ML	Sat Jan 14 17:14:06 2006 +0100
    12.3 @@ -60,22 +60,22 @@
    12.4  writeln"The following should fail, as they are false!";
    12.5  
    12.6  Goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
    12.7 -by tac handle ERROR => writeln"Failed, as expected";
    12.8 +by tac handle ERROR _ => writeln"Failed, as expected";
    12.9  (*Check that subgoals remain: proof failed.*)
   12.10  getgoal 1;
   12.11  
   12.12  Goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
   12.13 -by tac handle ERROR => writeln"Failed, as expected";
   12.14 +by tac handle ERROR _ => writeln"Failed, as expected";
   12.15  getgoal 1;
   12.16  
   12.17  Goal "?p : P(?a) --> (ALL x. P(x))";
   12.18 -by tac handle ERROR => writeln"Failed, as expected";
   12.19 +by tac handle ERROR _ => writeln"Failed, as expected";
   12.20  (*Check that subgoals remain: proof failed.*)
   12.21  getgoal 1;
   12.22  
   12.23  Goal
   12.24      "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
   12.25 -by tac handle ERROR => writeln"Failed, as expected";
   12.26 +by tac handle ERROR _ => writeln"Failed, as expected";
   12.27  getgoal 1;
   12.28  
   12.29  
    13.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jan 13 17:39:41 2006 +0100
    13.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Jan 14 17:14:06 2006 +0100
    13.3 @@ -212,17 +212,17 @@
    13.4  	fun F n =
    13.5  	    let
    13.6  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    13.7 -		val cu  = transform_error (read_cterm sign) (str,T)
    13.8 +		val cu  = read_cterm sign (str,T)
    13.9  	    in
   13.10  		if match cu
   13.11  		then quote str
   13.12  		else F (n+1)
   13.13  	    end
   13.14 -	    handle ERROR_MESSAGE mesg => F (n+1)
   13.15 +	    handle ERROR mesg => F (n+1)
   13.16      in
   13.17 -	transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F)) 0
   13.18 +      Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
   13.19      end
   13.20 -    handle ERROR_MESSAGE mesg => simple_smart_string_of_cterm ct
   13.21 +    handle ERROR mesg => simple_smart_string_of_cterm ct
   13.22   
   13.23  val smart_string_of_thm = smart_string_of_cterm o cprop_of
   13.24  
   13.25 @@ -457,11 +457,13 @@
   13.26  
   13.27  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
   13.28  
   13.29 -fun handle_error f d = transform_error f () handle ERROR_MESSAGE _ => d
   13.30 +val check_name_thy = theory "Main"
   13.31  
   13.32 -val check_name_thy = theory "Main"
   13.33 -fun valid_boundvarname s = handle_error (fn () => (read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT); true)) false 
   13.34 -fun valid_varname s = handle_error (fn () => (read_cterm check_name_thy (s, TypeInfer.logicT); true)) false 
   13.35 +fun valid_boundvarname s =
   13.36 +  can (fn () => read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
   13.37 +
   13.38 +fun valid_varname s =
   13.39 +  can (fn () => read_cterm check_name_thy (s, TypeInfer.logicT)) ();
   13.40  
   13.41  fun protect_varname s =
   13.42      if innocent_varname s andalso valid_varname s then s else
   13.43 @@ -1253,8 +1255,8 @@
   13.44  	case get_hol4_mapping thyname thmname thy of
   13.45  	    SOME (SOME thmname) =>
   13.46  	    let
   13.47 -		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
   13.48 -			   handle ERROR_MESSAGE _ =>
   13.49 +		val th1 = (SOME (PureThy.get_thm thy (Name thmname))
   13.50 +			   handle ERROR _ =>
   13.51  				  (case split_name thmname of
   13.52  				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
   13.53  							       handle _ => NONE)
   13.54 @@ -2123,7 +2125,8 @@
   13.55  
   13.56  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
   13.57      case HOL4DefThy.get thy of
   13.58 -	Replaying _ => (thy, handle_error (fn () => HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern")))) hth)
   13.59 +	Replaying _ => (thy,
   13.60 +          HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
   13.61        | _ => 
   13.62  	let
   13.63              val _ = message "TYPE_INTRO:"
    14.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 13 17:39:41 2006 +0100
    14.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 14 17:14:06 2006 +0100
    14.3 @@ -976,8 +976,8 @@
    14.4                  Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
    14.5                     map (dtyp_of_typ new_dts) cargs')],
    14.6                constr_syntax' @ [(cname, mx')], sorts'')
    14.7 -          end handle ERROR =>
    14.8 -            error ("The error above occured in constructor " ^ cname ^
    14.9 +          end handle ERROR msg =>
   14.10 +            cat_error msg ("The error above occured in constructor " ^ cname ^
   14.11                " of datatype " ^ tname);
   14.12  
   14.13          val (constrs', constr_syntax', sorts') =
    15.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 13 17:39:41 2006 +0100
    15.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 14 17:14:06 2006 +0100
    15.3 @@ -850,7 +850,7 @@
    15.4  
    15.5      val intr_names = map (fst o fst) intro_srcs;
    15.6      fun read_rule s = Thm.read_cterm thy (s, propT)
    15.7 -      handle ERROR => error ("The error(s) above occurred for " ^ s);
    15.8 +      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
    15.9      val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   15.10      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   15.11      val (cs', intr_ts') = unify_consts thy cs intr_ts;
    16.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jan 13 17:39:41 2006 +0100
    16.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 14 17:14:06 2006 +0100
    16.3 @@ -272,7 +272,7 @@
    16.4      val ((names, strings), srcss) = apfst split_list (split_list eqns);
    16.5      val atts = map (map (Attrib.global_attribute thy)) srcss;
    16.6      val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT))
    16.7 -      handle ERROR => error ("The error(s) above occurred for " ^ s)) strings;
    16.8 +      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
    16.9      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
   16.10        handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts;
   16.11      val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts
    17.1 --- a/src/HOL/Tools/record_package.ML	Fri Jan 13 17:39:41 2006 +0100
    17.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jan 14 17:14:06 2006 +0100
    17.3 @@ -2024,7 +2024,7 @@
    17.4      fun prep_inst T = snd (cert_typ sign ([], T));
    17.5  
    17.6      val parent = Option.map (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
    17.7 -      handle ERROR => error ("The error(s) above in parent record specification");
    17.8 +      handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
    17.9      val parents = add_parents thy parent [];
   17.10  
   17.11      val init_env =
   17.12 @@ -2036,8 +2036,8 @@
   17.13      (* fields *)
   17.14  
   17.15      fun prep_field (env, (c, raw_T, mx)) =
   17.16 -      let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
   17.17 -        error ("The error(s) above occured in field " ^ quote c)
   17.18 +      let val (env', T) = prep_typ sign (env, raw_T) handle ERROR msg =>
   17.19 +        cat_error msg ("The error(s) above occured in field " ^ quote c)
   17.20        in (env', (c, T, mx)) end;
   17.21  
   17.22      val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
   17.23 @@ -2090,7 +2090,7 @@
   17.24      if null errs then () else error (cat_lines errs)  ;
   17.25      thy |> record_definition (args, bname) parent parents bfields
   17.26    end
   17.27 -  handle ERROR => error ("Failed to define record " ^ quote bname);
   17.28 +  handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);
   17.29  
   17.30  val add_record = gen_add_record read_typ read_raw_parent;
   17.31  val add_record_i = gen_add_record cert_typ (K I);
    18.1 --- a/src/HOL/Tools/refute.ML	Fri Jan 13 17:39:41 2006 +0100
    18.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 14 17:14:06 2006 +0100
    18.3 @@ -466,7 +466,7 @@
    18.4  					case Type.lookup (typeSubs, v) of
    18.5  					  NONE =>
    18.6  						(* schematic type variable not instantiated *)
    18.7 -						raise ERROR
    18.8 +						error ""
    18.9  					| SOME typ =>
   18.10  						typ)) t
   18.11  		(* Term.term list * Term.typ -> Term.term list *)
   18.12 @@ -550,7 +550,7 @@
   18.13  							| NONE =>
   18.14  								get_typedefn axms
   18.15  						end
   18.16 -						handle ERROR           => get_typedefn axms
   18.17 +						handle ERROR _         => get_typedefn axms
   18.18  						     | MATCH           => get_typedefn axms
   18.19  						     | Type.TYPE_MATCH => get_typedefn axms)
   18.20  				in
   18.21 @@ -650,7 +650,7 @@
   18.22  							else
   18.23  								get_defn axms
   18.24  						end
   18.25 -						handle ERROR           => get_defn axms
   18.26 +						handle ERROR _         => get_defn axms
   18.27  						     | TERM _          => get_defn axms
   18.28  						     | Type.TYPE_MATCH => get_defn axms)
   18.29  					(* axiomatic type classes *)
    19.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Jan 13 17:39:41 2006 +0100
    19.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Jan 14 17:14:06 2006 +0100
    19.3 @@ -307,7 +307,7 @@
    19.4  				  []      => [xs1]
    19.5  				| (0::[]) => [xs1]
    19.6  				| (0::tl) => xs1 :: clauses tl
    19.7 -				| _       => raise ERROR  (* this cannot happen *)
    19.8 +				| _       => sys_error "this cannot happen"
    19.9  			end
   19.10  		(* int -> PropLogic.prop_formula *)
   19.11  		fun literal_from_int i =
   19.12 @@ -457,7 +457,7 @@
   19.13  			  | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
   19.14  			  (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   19.15  			  (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   19.16 -			  | forced_vars _                 = raise ERROR  (* formula is not in negation normal form *)
   19.17 +			  | forced_vars _                 = error "formula is not in negation normal form"
   19.18  			(* int list -> prop_formula -> (int list * prop_formula) *)
   19.19  			fun eval_and_force xs fm =
   19.20  			let
   19.21 @@ -528,7 +528,7 @@
   19.22  				(if name="dpll" orelse name="enumerate" then
   19.23  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   19.24  				else
   19.25 -					debug ("Using SAT solver " ^ quote name ^ "."));
   19.26 +					Output.debug ("Using SAT solver " ^ quote name ^ "."));
   19.27  				(* apply 'solver' to 'fm' *)
   19.28  				solver fm
   19.29  					handle SatSolver.NOT_CONFIGURED => loop solvers
    20.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jan 13 17:39:41 2006 +0100
    20.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Jan 14 17:14:06 2006 +0100
    20.3 @@ -93,8 +93,8 @@
    20.4  
    20.5  fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
    20.6  
    20.7 -fun err_in_typedef name =
    20.8 -  error ("The error(s) above occurred in typedef " ^ quote name);
    20.9 +fun err_in_typedef msg name =
   20.10 +  cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
   20.11  
   20.12  fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
   20.13    let
   20.14 @@ -224,7 +224,7 @@
   20.15        setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
   20.16  
   20.17    in (cset, goal, goal_pat, typedef_result) end
   20.18 -  handle ERROR => err_in_typedef name;
   20.19 +  handle ERROR msg => err_in_typedef msg name;
   20.20  
   20.21  
   20.22  (* add_typedef interfaces *)
   20.23 @@ -237,8 +237,8 @@
   20.24      val (cset, goal, _, typedef_result) =
   20.25        prepare_typedef prep_term def name typ set opt_morphs thy;
   20.26      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
   20.27 -    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
   20.28 -      error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   20.29 +    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
   20.30 +      cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   20.31      val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   20.32    in (thy', result) end;
   20.33  
    21.1 --- a/src/HOL/ex/ROOT.ML	Fri Jan 13 17:39:41 2006 +0100
    21.2 +++ b/src/HOL/ex/ROOT.ML	Sat Jan 14 17:14:06 2006 +0100
    21.3 @@ -45,7 +45,7 @@
    21.4  if_svc_enabled time_use_thy "svc_test";
    21.5  
    21.6  (* requires zChaff with proof generation to be installed: *)
    21.7 -time_use_thy "SAT_Examples" handle ERROR => ();
    21.8 +try time_use_thy "SAT_Examples";
    21.9  
   21.10  (* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
   21.11  if getenv "ZCHAFF_HOME" <> "" then
    22.1 --- a/src/HOLCF/adm_tac.ML	Fri Jan 13 17:39:41 2006 +0100
    22.2 +++ b/src/HOLCF/adm_tac.ML	Sat Jan 14 17:14:06 2006 +0100
    22.3 @@ -104,7 +104,7 @@
    22.4         val t' = mk_all params (Logic.list_implies (prems, t));
    22.5         val thm = Goal.prove sign [] [] t' (K (tac 1));
    22.6    in (ts, thm)::l end
    22.7 -  handle ERROR_MESSAGE _ => l;
    22.8 +  handle ERROR _ => l;
    22.9  
   22.10  
   22.11  (*** instantiation of adm_subst theorem (a bit tricky) ***)
    23.1 --- a/src/HOLCF/cont_consts.ML	Fri Jan 13 17:39:41 2006 +0100
    23.2 +++ b/src/HOLCF/cont_consts.ML	Sat Jan 14 17:14:06 2006 +0100
    23.3 @@ -72,7 +72,7 @@
    23.4  fun is_contconst (_,_,NoSyn   ) = false
    23.5  |   is_contconst (_,_,Binder _) = false
    23.6  |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    23.7 -                         handle ERROR => error ("in mixfix annotation for " ^
    23.8 +                         handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
    23.9                                                 quote (Syntax.const_name c mx));
   23.10  
   23.11  
    24.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 13 17:39:41 2006 +0100
    24.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jan 14 17:14:06 2006 +0100
    24.3 @@ -587,7 +587,7 @@
    24.4                                  strip_tac 1,
    24.5                                  rtac (rewrite_rule axs_take_def finite_ind) 1,
    24.6                                  ind_prems_tac prems])
    24.7 -  handle ERROR => (warning "Cannot prove infinite induction rule"; refl))
    24.8 +  handle ERROR _ => (warning "Cannot prove infinite induction rule"; refl))
    24.9  end; (* local *)
   24.10  
   24.11  (* ----- theorem concerning coinduction ------------------------------------- *)
    25.1 --- a/src/HOLCF/pcpodef_package.ML	Fri Jan 13 17:39:41 2006 +0100
    25.2 +++ b/src/HOLCF/pcpodef_package.ML	Sat Jan 14 17:14:06 2006 +0100
    25.3 @@ -53,8 +53,8 @@
    25.4  
    25.5  fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
    25.6  
    25.7 -fun err_in_cpodef name =
    25.8 -  error ("The error(s) above occurred in cpodef " ^ quote name);
    25.9 +fun err_in_cpodef msg name =
   25.10 +  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
   25.11  
   25.12  fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
   25.13  fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
   25.14 @@ -168,7 +168,7 @@
   25.15        end;
   25.16    
   25.17    in (goal, if pcpo then pcpodef_result else cpodef_result) end
   25.18 -  handle ERROR => err_in_cpodef name;
   25.19 +  handle ERROR msg => err_in_cpodef msg name;
   25.20  
   25.21  (* cpodef_proof interface *)
   25.22  
    26.1 --- a/src/Provers/induct_method.ML	Fri Jan 13 17:39:41 2006 +0100
    26.2 +++ b/src/Provers/induct_method.ML	Sat Jan 14 17:14:06 2006 +0100
    26.3 @@ -53,11 +53,11 @@
    26.4  
    26.5  fun align_left msg xs ys =
    26.6    let val m = length xs and n = length ys
    26.7 -  in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
    26.8 +  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
    26.9  
   26.10  fun align_right msg xs ys =
   26.11    let val m = length xs and n = length ys
   26.12 -  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
   26.13 +  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
   26.14  
   26.15  
   26.16  (* prep_inst *)
   26.17 @@ -72,7 +72,7 @@
   26.18              val ct = cert (tune t);
   26.19            in
   26.20              if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
   26.21 -            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
   26.22 +            else error (Pretty.string_of (Pretty.block
   26.23               [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
   26.24                Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
   26.25                Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    27.1 --- a/src/Pure/General/file.ML	Fri Jan 13 17:39:41 2006 +0100
    27.2 +++ b/src/Pure/General/file.ML	Sat Jan 14 17:14:06 2006 +0100
    27.3 @@ -147,6 +147,6 @@
    27.4  
    27.5  (* use ML files *)
    27.6  
    27.7 -val use = use o platform_path;
    27.8 +val use = Output.toplevel_errors (use o platform_path);
    27.9  
   27.10  end;
    28.1 --- a/src/Pure/IsaPlanner/isand.ML	Fri Jan 13 17:39:41 2006 +0100
    28.2 +++ b/src/Pure/IsaPlanner/isand.ML	Sat Jan 14 17:14:06 2006 +0100
    28.3 @@ -324,8 +324,7 @@
    28.4  (* lookup type of a free var name from a list *)
    28.5  fun lookupfree vs vn  = 
    28.6      case Library.find_first (fn (n,ty) => n = vn) vs of 
    28.7 -      NONE => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: " 
    28.8 -                    ^ vn ^ " does not occur in the term")
    28.9 +      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
   28.10      | SOME x => x;
   28.11  in
   28.12  fun export_back (export {fixes = vs, assumes = hprems, 
   28.13 @@ -523,7 +522,7 @@
   28.14        val t = (prop_of th); 
   28.15        val gt = Logic.get_goal t i;
   28.16        val _ = case Term.strip_all_vars gt of [] => () 
   28.17 -              | _ => raise ERROR_MESSAGE "assume_prems: goal has params"
   28.18 +              | _ => error "assume_prems: goal has params"
   28.19        val body = gt;
   28.20        val prems = Logic.strip_imp_prems body;
   28.21        val concl = Logic.strip_imp_concl body;
    29.1 --- a/src/Pure/Isar/attrib.ML	Fri Jan 13 17:39:41 2006 +0100
    29.2 +++ b/src/Pure/Isar/attrib.ML	Sat Jan 14 17:14:06 2006 +0100
    29.3 @@ -171,7 +171,7 @@
    29.4    at the thm structure.*)
    29.5  
    29.6  fun crude_closure ctxt src =
    29.7 - (try (transform_error (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl))) ();
    29.8 + (try (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl)) ();
    29.9    Args.closure src);
   29.10  
   29.11  
    30.1 --- a/src/Pure/Isar/calculation.ML	Fri Jan 13 17:39:41 2006 +0100
    30.2 +++ b/src/Pure/Isar/calculation.ML	Sat Jan 14 17:14:06 2006 +0100
    30.3 @@ -109,7 +109,7 @@
    30.4  
    30.5  (** proof commands **)
    30.6  
    30.7 -fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
    30.8 +fun err_if b msg = if b then error msg else ();
    30.9  
   30.10  fun assert_sane final =
   30.11    if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   30.12 @@ -147,8 +147,8 @@
   30.13          NONE => (true, Seq.single facts)
   30.14        | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   30.15    in
   30.16 -    err_if state (initial andalso final) "No calculation yet";
   30.17 -    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   30.18 +    err_if (initial andalso final) "No calculation yet";
   30.19 +    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   30.20      calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   30.21          state |> maintain_calculation final calc))
   30.22    end;
   30.23 @@ -170,7 +170,7 @@
   30.24        | SOME thms => (false, thms));
   30.25      val calc = thms @ facts;
   30.26    in
   30.27 -    err_if state (initial andalso final) "No calculation yet";
   30.28 +    err_if (initial andalso final) "No calculation yet";
   30.29      print_calculation int (Proof.context_of state) calc;
   30.30      state |> maintain_calculation final calc
   30.31    end;
    31.1 --- a/src/Pure/Isar/isar_output.ML	Fri Jan 13 17:39:41 2006 +0100
    31.2 +++ b/src/Pure/Isar/isar_output.ML	Sat Jan 14 17:14:06 2006 +0100
    31.3 @@ -144,8 +144,10 @@
    31.4  in
    31.5  
    31.6  fun antiq_args lex (s, pos) =
    31.7 -  (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
    31.8 -    error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
    31.9 +  let
   31.10 +    fun err msg = cat_error msg
   31.11 +      ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
   31.12 +  in (case antiq_args_aux lex (s, pos) of [x] => x | _ => err "") handle ERROR msg => err msg end;
   31.13  
   31.14  end;
   31.15  
    32.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jan 13 17:39:41 2006 +0100
    32.2 +++ b/src/Pure/Isar/isar_thy.ML	Sat Jan 14 17:14:06 2006 +0100
    32.3 @@ -134,8 +134,8 @@
    32.4  (* global endings *)
    32.5  
    32.6  fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
    32.7 - (Proof.assert_bottom true state handle Proof.STATE _ => raise Toplevel.UNDEF;
    32.8 -  ending int state));
    32.9 +  if can (Proof.assert_bottom true) state then ending int state
   32.10 +  else raise Toplevel.UNDEF);
   32.11  
   32.12  fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
   32.13  val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
    33.1 --- a/src/Pure/Isar/locale.ML	Fri Jan 13 17:39:41 2006 +0100
    33.2 +++ b/src/Pure/Isar/locale.ML	Sat Jan 14 17:14:06 2006 +0100
    33.3 @@ -475,7 +475,7 @@
    33.4        if forall (equal "" o #1) ids then msg
    33.5        else msg ^ "\n" ^ Pretty.string_of (Pretty.block
    33.6          (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
    33.7 -  in raise ProofContext.CONTEXT (err_msg, ctxt) end;
    33.8 +  in error err_msg end;
    33.9  
   33.10  fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   33.11  
   33.12 @@ -668,7 +668,7 @@
   33.13      fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
   33.14        | renaming (NONE :: xs) (y :: ys) = renaming xs ys
   33.15        | renaming [] _ = []
   33.16 -      | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
   33.17 +      | renaming xs [] = error ("Too many arguments in renaming: " ^
   33.18            commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
   33.19  
   33.20      fun rename_parms top ren ((name, ps), (parms, mode)) =
   33.21 @@ -749,7 +749,7 @@
   33.22            let
   33.23              val (ids', parms', syn') = identify top e;
   33.24              val ren = renaming xs parms'
   33.25 -              handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
   33.26 +              handle ERROR msg => err_in_locale' ctxt msg ids';
   33.27  
   33.28              val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   33.29              val parms'' = distinct (List.concat (map (#2 o #1) ids''));
   33.30 @@ -869,7 +869,7 @@
   33.31      val thy = ProofContext.theory_of ctxt;
   33.32      val ((ctxt', _), res) =
   33.33          foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
   33.34 -      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   33.35 +      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
   33.36      val ctxt'' = if name = "" then ctxt'
   33.37            else let
   33.38                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   33.39 @@ -992,8 +992,7 @@
   33.40        (case elems of
   33.41          Int es => foldl_map declare_int_elem (ctxt, es)
   33.42        | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
   33.43 -      handle ProofContext.CONTEXT (msg, ctxt) =>
   33.44 -        err_in_locale ctxt msg [(name, map fst ps)]
   33.45 +      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
   33.46      in (ctxt', propps) end
   33.47    | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
   33.48  
   33.49 @@ -1102,8 +1101,7 @@
   33.50            in Term.list_all_free (frees, t) end;
   33.51  
   33.52          fun no_binds [] = []
   33.53 -          | no_binds _ =
   33.54 -              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
   33.55 +          | no_binds _ = error "Illegal term bindings in locale element";
   33.56        in
   33.57          (case elem of
   33.58            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   33.59 @@ -1244,16 +1242,15 @@
   33.60  
   33.61  local
   33.62  
   33.63 -fun prep_name ctxt name =
   33.64 -  if NameSpace.is_qualified name then
   33.65 -    raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   33.66 +fun prep_name name =
   33.67 +  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   33.68    else name;
   33.69  
   33.70  fun prep_facts _ _ ctxt (Int elem) =
   33.71        Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
   33.72    | prep_facts get intern ctxt (Ext elem) = elem |> Element.map_ctxt
   33.73       {var = I, typ = I, term = I,
   33.74 -      name = prep_name ctxt,
   33.75 +      name = prep_name,
   33.76        fact = get ctxt,
   33.77        attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   33.78  
    34.1 --- a/src/Pure/Isar/obtain.ML	Fri Jan 13 17:39:41 2006 +0100
    34.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 17:14:06 2006 +0100
    34.3 @@ -52,7 +52,7 @@
    34.4  
    34.5  (** obtain_export **)
    34.6  
    34.7 -fun obtain_export state parms rule cprops thm =
    34.8 +fun obtain_export ctxt parms rule cprops thm =
    34.9    let
   34.10      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
   34.11      val cparms = map (Thm.cterm_of thy) parms;
   34.12 @@ -67,10 +67,10 @@
   34.13      val bads = parms inter (Term.term_frees concl);
   34.14    in
   34.15      if not (null bads) then
   34.16 -      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
   34.17 -        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
   34.18 +      error ("Conclusion contains obtained parameters: " ^
   34.19 +        space_implode " " (map (ProofContext.string_of_term ctxt) bads))
   34.20      else if not (ObjectLogic.is_judgment thy concl) then
   34.21 -      raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state)
   34.22 +      error "Conclusion in obtained context must be object-logic judgments"
   34.23      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
   34.24    end;
   34.25  
   34.26 @@ -92,6 +92,7 @@
   34.27    let
   34.28      val _ = Proof.assert_forward_or_chain state;
   34.29      val ctxt = Proof.context_of state;
   34.30 +    val thy = Proof.theory_of state;
   34.31      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   34.32  
   34.33      (*obtain vars*)
   34.34 @@ -103,7 +104,7 @@
   34.35      (*obtain asms*)
   34.36      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   34.37      val asm_props = List.concat (map (map fst) proppss);
   34.38 -    val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss;
   34.39 +    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
   34.40  
   34.41      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   34.42  
   34.43 @@ -129,7 +130,7 @@
   34.44        Proof.local_qed (NONE, false)
   34.45        #> Seq.map (`Proof.the_fact #-> (fn rule =>
   34.46          Proof.fix_i (xs ~~ Ts)
   34.47 -        #> Proof.assm_i (K (obtain_export state parms rule)) asms));
   34.48 +        #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
   34.49    in
   34.50      state
   34.51      |> Proof.enter_forward
   34.52 @@ -157,14 +158,13 @@
   34.53  
   34.54  local
   34.55  
   34.56 -fun match_params state vars rule =
   34.57 +fun match_params ctxt vars rule =
   34.58    let
   34.59 -    val ctxt = Proof.context_of state;
   34.60 -    val thy = Proof.theory_of state;
   34.61 +    val thy = ProofContext.theory_of ctxt;
   34.62      val string_of_typ = ProofContext.string_of_typ ctxt;
   34.63      val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
   34.64  
   34.65 -    fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state);
   34.66 +    fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
   34.67  
   34.68      val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
   34.69      val m = length vars;
   34.70 @@ -214,26 +214,23 @@
   34.71          [prem] =>
   34.72            if Thm.concl_of th aconv thesis andalso
   34.73              Logic.strip_assums_concl prem aconv thesis then ()
   34.74 -          else raise Proof.STATE ("Guessed a different clause:\n" ^
   34.75 -            ProofContext.string_of_thm ctxt th, state)
   34.76 -      | [] => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
   34.77 -      | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
   34.78 -        ProofContext.string_of_thm ctxt th, state));
   34.79 +          else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
   34.80 +      | [] => error "Goal solved -- nothing guessed."
   34.81 +      | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   34.82  
   34.83      fun guess_context raw_rule =
   34.84        let
   34.85 -        val (parms, rule) = match_params state (map (fn (x, T, _) => (x, T)) vars) raw_rule;
   34.86 +        val (parms, rule) = match_params ctxt (map (fn (x, T, _) => (x, T)) vars) raw_rule;
   34.87          val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
   34.88          val ts = map (bind o Free) parms;
   34.89          val ps = map dest_Free ts;
   34.90          val asms =
   34.91            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   34.92            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
   34.93 -        val _ = conditional (null asms) (fn () =>
   34.94 -          raise Proof.STATE ("Trivial result -- nothing guessed", state));
   34.95 +        val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
   34.96        in
   34.97          Proof.fix_i (map (apsnd SOME) parms)
   34.98 -        #> Proof.assm_i (K (obtain_export state ts rule)) [(("", []), asms)]
   34.99 +        #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
  34.100          #> Proof.add_binds_i AutoBind.no_facts
  34.101        end;
  34.102  
    35.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 13 17:39:41 2006 +0100
    35.2 +++ b/src/Pure/Isar/proof.ML	Sat Jan 14 17:14:06 2006 +0100
    35.3 @@ -10,7 +10,6 @@
    35.4    type context (*= Context.proof*)
    35.5    type method (*= Method.method*)
    35.6    type state
    35.7 -  exception STATE of string * state
    35.8    val init: context -> state
    35.9    val level: state -> int
   35.10    val assert_bottom: bool -> state -> state
   35.11 @@ -164,8 +163,6 @@
   35.12        (thm list list -> state -> state Seq.seq) *
   35.13        (thm list list -> theory -> theory)};
   35.14  
   35.15 -exception STATE of string * state;
   35.16 -
   35.17  fun make_goal (statement, using, goal, before_qed, after_qed) =
   35.18    Goal {statement = statement, using = using, goal = goal,
   35.19      before_qed = before_qed, after_qed = after_qed};
   35.20 @@ -189,15 +186,15 @@
   35.21  
   35.22  fun open_block (State st) = State (Stack.push st);
   35.23  
   35.24 -fun close_block (state as State st) = State (Stack.pop st)
   35.25 -  handle Empty => raise STATE ("Unbalanced block parentheses", state);
   35.26 +fun close_block (State st) = State (Stack.pop st)
   35.27 +  handle Empty => error "Unbalanced block parentheses";
   35.28  
   35.29  fun level (State st) = Stack.level st;
   35.30  
   35.31  fun assert_bottom b state =
   35.32    let val b' = (level state <= 2) in
   35.33 -    if b andalso not b' then raise STATE ("Not at bottom of proof!", state)
   35.34 -    else if not b andalso b' then raise STATE ("Already at bottom of proof!", state)
   35.35 +    if b andalso not b' then error "Not at bottom of proof!"
   35.36 +    else if not b andalso b' then error "Already at bottom of proof!"
   35.37      else state
   35.38    end;
   35.39  
   35.40 @@ -226,11 +223,11 @@
   35.41  
   35.42  fun the_facts state =
   35.43    (case get_facts state of SOME facts => facts
   35.44 -  | NONE => raise STATE ("No current facts available", state));
   35.45 +  | NONE => error "No current facts available");
   35.46  
   35.47  fun the_fact state =
   35.48    (case the_facts state of [thm] => thm
   35.49 -  | _ => raise STATE ("Single theorem expected", state));
   35.50 +  | _ => error "Single theorem expected");
   35.51  
   35.52  fun put_facts facts =
   35.53    map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
   35.54 @@ -258,8 +255,7 @@
   35.55  fun assert_mode pred state =
   35.56    let val mode = get_mode state in
   35.57      if pred mode then state
   35.58 -    else raise STATE ("Illegal application of proof command in "
   35.59 -      ^ quote (mode_name mode) ^ " mode", state)
   35.60 +    else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
   35.61    end;
   35.62  
   35.63  val assert_forward = assert_mode (equal Forward);
   35.64 @@ -278,12 +274,12 @@
   35.65  fun current_goal state =
   35.66    (case current state of
   35.67      {context, goal = SOME (Goal goal), ...} => (context, goal)
   35.68 -  | _ => raise STATE ("No current goal!", state));
   35.69 +  | _ => error "No current goal!");
   35.70  
   35.71  fun assert_current_goal g state =
   35.72    let val g' = can current_goal state in
   35.73 -    if g andalso not g' then raise STATE ("No goal in this block!", state)
   35.74 -    else if not g andalso g' then raise STATE ("Goal present in this block!", state)
   35.75 +    if g andalso not g' then error "No goal in this block!"
   35.76 +    else if not g andalso g' then error "Goal present in this block!"
   35.77      else state
   35.78    end;
   35.79  
   35.80 @@ -311,8 +307,7 @@
   35.81    fun find i state =
   35.82      (case try current_goal state of
   35.83        SOME (ctxt, goal) => (ctxt, (i, goal))
   35.84 -    | NONE => find (i + 1) (close_block state
   35.85 -        handle STATE _ => raise STATE ("No goal present", state)));
   35.86 +    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
   35.87  in val find_goal = find 0 end;
   35.88  
   35.89  fun get_goal state =
   35.90 @@ -394,7 +389,7 @@
   35.91  
   35.92  fun check_theory thy state =
   35.93    if subthy (thy, theory_of state) then state
   35.94 -  else raise STATE ("Bad theory of method result: " ^ Context.str_of_thy thy, state);
   35.95 +  else error ("Bad theory of method result: " ^ Context.str_of_thy thy);
   35.96  
   35.97  fun apply_method current_context meth_fun state =
   35.98    let
   35.99 @@ -466,23 +461,22 @@
  35.100  fun conclude_goal state goal propss =
  35.101    let
  35.102      val ctxt = context_of state;
  35.103 -    fun err msg = raise STATE (msg, state);
  35.104  
  35.105      val ngoals = Thm.nprems_of goal;
  35.106      val _ = conditional (ngoals > 0) (fn () =>
  35.107 -      err (Pretty.string_of (Pretty.chunks
  35.108 +      error (Pretty.string_of (Pretty.chunks
  35.109          (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
  35.110            [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
  35.111  
  35.112      val {hyps, thy, ...} = Thm.rep_thm goal;
  35.113      val bad_hyps = fold (remove (op aconv)) (ProofContext.assms_of ctxt) hyps;
  35.114 -    val _ = conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
  35.115 +    val _ = conditional (not (null bad_hyps)) (fn () => error ("Additional hypotheses:\n" ^
  35.116          cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
  35.117  
  35.118      val th = Goal.conclude goal;
  35.119      val _ = conditional (not (Pattern.matches thy
  35.120          (Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
  35.121 -      err ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
  35.122 +      error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
  35.123    in Drule.conj_elim_precise (map length propss) th end;
  35.124  
  35.125  
  35.126 @@ -759,8 +753,8 @@
  35.127  
  35.128  fun check_tvars props state =
  35.129    (case fold Term.add_tvars props [] of [] => ()
  35.130 -  | tvars => raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
  35.131 -      commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars), state));
  35.132 +  | tvars => error ("Goal statement contains illegal schematic type variable(s): " ^
  35.133 +      commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars)));
  35.134  
  35.135  fun check_vars props state =
  35.136    (case fold Term.add_vars props [] of [] => ()
  35.137 @@ -873,9 +867,9 @@
  35.138        before_qed (K Seq.single, after_qed') propp
  35.139    end;
  35.140  
  35.141 -fun check_result msg state sq =
  35.142 +fun check_result msg sq =
  35.143    (case Seq.pull sq of
  35.144 -    NONE => raise STATE (msg, state)
  35.145 +    NONE => error msg
  35.146    | SOME res => Seq.cons res);
  35.147  
  35.148  fun global_qeds txt =
  35.149 @@ -886,11 +880,10 @@
  35.150      |> Seq.map (rpair (context_of state)))
  35.151    |> Seq.DETERM;   (*backtracking may destroy theory!*)
  35.152  
  35.153 -fun global_qed txt state =
  35.154 -  state
  35.155 -  |> global_qeds txt
  35.156 -  |> check_result "Failed to finish proof" state
  35.157 -  |> Seq.hd;
  35.158 +fun global_qed txt =
  35.159 +  global_qeds txt
  35.160 +  #> check_result "Failed to finish proof"
  35.161 +  #> Seq.hd;
  35.162  
  35.163  
  35.164  (* concluding steps *)
  35.165 @@ -903,13 +896,12 @@
  35.166  val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
  35.167  fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
  35.168  
  35.169 -fun global_term_proof immed (text, opt_text) state =
  35.170 -  state
  35.171 -  |> proof (SOME text)
  35.172 -  |> check_result "Terminal proof method failed" state
  35.173 -  |> Seq.maps (global_qeds (opt_text, immed))
  35.174 -  |> check_result "Failed to finish proof (after successful terminal method)" state
  35.175 -  |> Seq.hd;
  35.176 +fun global_term_proof immed (text, opt_text) =
  35.177 +  proof (SOME text)
  35.178 +  #> check_result "Terminal proof method failed"
  35.179 +  #> Seq.maps (global_qeds (opt_text, immed))
  35.180 +  #> check_result "Failed to finish proof (after successful terminal method)"
  35.181 +  #> Seq.hd;
  35.182  
  35.183  val global_terminal_proof = global_term_proof true;
  35.184  val global_default_proof = global_terminal_proof (Method.default_text, NONE);
  35.185 @@ -944,7 +936,6 @@
  35.186        (Seq.pull oo local_skip_proof) true
  35.187        |> setmp testing true
  35.188        |> setmp proofs 0
  35.189 -      |> transform_error
  35.190        |> capture;
  35.191  
  35.192      fun after_qed' results =
  35.193 @@ -956,7 +947,7 @@
  35.194      |> K int ? (fn goal_state =>
  35.195        (case test_proof goal_state of
  35.196          Result (SOME _) => goal_state
  35.197 -      | Result NONE => raise STATE (fail_msg (context_of goal_state), goal_state)
  35.198 +      | Result NONE => error (fail_msg (context_of goal_state))
  35.199        | Exn Interrupt => raise Interrupt
  35.200        | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))
  35.201    end;
    36.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jan 13 17:39:41 2006 +0100
    36.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jan 14 17:14:06 2006 +0100
    36.3 @@ -11,7 +11,6 @@
    36.4  sig
    36.5    type context (*= Context.proof*)
    36.6    type export
    36.7 -  exception CONTEXT of string * context
    36.8    val theory_of: context -> theory
    36.9    val init: theory -> context
   36.10    val set_body: bool -> context -> context
   36.11 @@ -161,7 +160,6 @@
   36.12  struct
   36.13  
   36.14  type context = Context.proof;
   36.15 -exception CONTEXT = Context.PROOF;
   36.16  
   36.17  val theory_of = Context.theory_of_proof;
   36.18  val init = Context.init_proof;
   36.19 @@ -289,10 +287,10 @@
   36.20  
   36.21  local
   36.22  
   36.23 -fun check_mixfix ctxt (x, _, mx) =
   36.24 +fun check_mixfix (x, _, mx) =
   36.25    if mx <> NoSyn andalso mx <> Structure andalso
   36.26        (can Syntax.dest_internal x orelse can Syntax.dest_skolem x) then
   36.27 -    raise CONTEXT ("Illegal mixfix syntax for internal/skolem constant " ^ quote x, ctxt)
   36.28 +    error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
   36.29    else ();
   36.30  
   36.31  fun mixfix x NONE mx = (Syntax.fixedN ^ x, TypeInfer.mixfixT mx, Syntax.fix_mixfix x mx)
   36.32 @@ -329,7 +327,7 @@
   36.33  
   36.34      val is_logtype = Sign.is_logtype thy;
   36.35      val structs' = structs @ List.mapPartial prep_struct decls;
   36.36 -    val mxs = List.mapPartial (tap (check_mixfix ctxt) #> prep_mixfix) decls;
   36.37 +    val mxs = List.mapPartial (tap check_mixfix #> prep_mixfix) decls;
   36.38      val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
   36.39  
   36.40      val extend =
   36.41 @@ -408,11 +406,11 @@
   36.42  fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1);
   36.43  
   36.44  fun infer_type ctxt x =
   36.45 -  (case try (transform_error (fn () =>
   36.46 +  (case try (fn () =>
   36.47        Sign.infer_types (pp ctxt) (theory_of ctxt) (def_type ctxt false) (def_sort ctxt)
   36.48 -        (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT))) () of
   36.49 +        (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of
   36.50      SOME (Free (_, T), _) => T
   36.51 -  | _ => raise CONTEXT ("Failed to infer type of fixed variable " ^ quote x, ctxt));
   36.52 +  | _ => error ("Failed to infer type of fixed variable " ^ quote x));
   36.53  
   36.54  
   36.55  
   36.56 @@ -421,12 +419,10 @@
   36.57  local
   36.58  
   36.59  fun read_typ_aux read ctxt s =
   36.60 -  transform_error (read (syn_of ctxt) (theory_of ctxt, def_sort ctxt)) s
   36.61 -    handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
   36.62 +  read (syn_of ctxt) (theory_of ctxt, def_sort ctxt) s;
   36.63  
   36.64  fun cert_typ_aux cert ctxt raw_T =
   36.65 -  cert (theory_of ctxt) raw_T
   36.66 -    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
   36.67 +  cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
   36.68  
   36.69  in
   36.70  
   36.71 @@ -445,11 +441,11 @@
   36.72  val lookup_skolem = AList.lookup (op =) o fixes_of;
   36.73  fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
   36.74  
   36.75 -fun no_skolem internal ctxt x =
   36.76 +fun no_skolem internal x =
   36.77    if can Syntax.dest_skolem x then
   36.78 -    raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   36.79 +    error ("Illegal reference to internal Skolem constant: " ^ quote x)
   36.80    else if not internal andalso can Syntax.dest_internal x then
   36.81 -    raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt)
   36.82 +    error ("Illegal reference to internal variable: " ^ quote x)
   36.83    else x;
   36.84  
   36.85  fun intern_skolem ctxt internal =
   36.86 @@ -457,7 +453,7 @@
   36.87      fun intern (t as Free (x, T)) =
   36.88            if internal x then t
   36.89            else
   36.90 -            (case lookup_skolem ctxt (no_skolem false ctxt x) of
   36.91 +            (case lookup_skolem ctxt (no_skolem false x) of
   36.92                SOME x' => Free (x', T)
   36.93              | NONE => t)
   36.94        | intern (t $ u) = intern t $ intern u
   36.95 @@ -546,7 +542,7 @@
   36.96                in norm u' handle SAME => u' end
   36.97            | NONE =>
   36.98              if schematic then raise SAME
   36.99 -            else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
  36.100 +            else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi))
  36.101        | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
  36.102        | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
  36.103        | norm (f $ t) =
  36.104 @@ -567,8 +563,8 @@
  36.105        in next := i; u end
  36.106    end;
  36.107  
  36.108 -fun reject_dummies ctxt t = Term.no_dummy_patterns t
  36.109 -  handle TERM _ => raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
  36.110 +fun reject_dummies t = Term.no_dummy_patterns t
  36.111 +  handle TERM _ => error "Illegal dummy pattern(s) in term";
  36.112  
  36.113  
  36.114  (* read terms *)
  36.115 @@ -584,12 +580,11 @@
  36.116      val sorts = append_env (def_sort ctxt) more_sorts;
  36.117      val used = used_types ctxt @ more_used;
  36.118    in
  36.119 -    (transform_error (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used)) s
  36.120 -      handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
  36.121 -        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
  36.122 +    (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used) s
  36.123 +      handle TERM (msg, _) => error msg)
  36.124      |> app (intern_skolem ctxt internal)
  36.125      |> app (if pattern then I else norm_term ctxt schematic)
  36.126 -    |> app (if pattern then prepare_dummies else reject_dummies ctxt)
  36.127 +    |> app (if pattern then prepare_dummies else reject_dummies)
  36.128    end;
  36.129  
  36.130  fun gen_read read app pattern schematic ctxt =
  36.131 @@ -623,8 +618,8 @@
  36.132  fun gen_cert cert pattern schematic ctxt t = t
  36.133    |> (if pattern then I else norm_term ctxt schematic)
  36.134    |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
  36.135 -    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt)
  36.136 -      | TERM (msg, _) => raise CONTEXT (msg, ctxt));
  36.137 +    handle TYPE (msg, _, _) => error msg
  36.138 +      | TERM (msg, _) => error msg);
  36.139  
  36.140  val certify_term = #1 ooo Sign.certify_term;
  36.141  val certify_prop = #1 ooo Sign.certify_prop;
  36.142 @@ -824,7 +819,7 @@
  36.143  fun simult_matches ctxt [] = []
  36.144    | simult_matches ctxt pairs =
  36.145        let
  36.146 -        fun fail () = raise CONTEXT ("Pattern match failed!", ctxt);
  36.147 +        fun fail () = error "Pattern match failed!";
  36.148  
  36.149          val maxidx = fold (fn (t1, t2) => fn i =>
  36.150            Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
  36.151 @@ -970,8 +965,7 @@
  36.152        let
  36.153          val thy = theory_of ctxt;
  36.154          val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt)))
  36.155 -          handle ERROR_MESSAGE msg =>
  36.156 -            raise CONTEXT (msg ^ "\nFailed to retrieve literal fact.", ctxt);
  36.157 +          handle ERROR msg => cat_error msg "Failed to retrieve literal fact.";
  36.158        in pick "" [th] end
  36.159    | retrieve_thms from_thy pick ctxt xthmref =
  36.160        let
  36.161 @@ -994,7 +988,7 @@
  36.162  (* valid_thms *)
  36.163  
  36.164  fun valid_thms ctxt (name, ths) =
  36.165 -  (case try (transform_error (fn () => get_thms ctxt (Name name))) () of
  36.166 +  (case try (fn () => get_thms ctxt (Name name)) () of
  36.167      NONE => false
  36.168    | SOME ths' => Thm.eq_thms (ths, ths'));
  36.169  
  36.170 @@ -1078,13 +1072,13 @@
  36.171        val x = Syntax.const_name raw_x raw_mx;
  36.172        val mx = Syntax.fix_mixfix raw_x raw_mx;
  36.173        val _ =
  36.174 -        if not legacy andalso not (Syntax.is_identifier (no_skolem internal ctxt x)) then
  36.175 -          raise CONTEXT ("Illegal variable name: " ^ quote x, ctxt)
  36.176 +        if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then
  36.177 +          error ("Illegal variable name: " ^ quote x)
  36.178          else ();
  36.179  
  36.180        fun cond_tvars T =
  36.181          if internal then T
  36.182 -        else Type.no_tvars T handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
  36.183 +        else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
  36.184        val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
  36.185        val var = (x, opt_T, mx);
  36.186      in (var, ctxt |> declare_var var) end);
  36.187 @@ -1104,7 +1098,7 @@
  36.188  local
  36.189  
  36.190  fun no_dups _ [] = ()
  36.191 -  | no_dups ctxt dups = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote dups, ctxt);
  36.192 +  | no_dups ctxt dups = error ("Duplicate variable(s): " ^ commas_quote dups);
  36.193  
  36.194  fun gen_fixes prep raw_vars ctxt =
  36.195    let
  36.196 @@ -1227,8 +1221,8 @@
  36.197  
  36.198  fun cert_def ctxt eq =
  36.199    let
  36.200 -    fun err msg = raise CONTEXT (msg ^
  36.201 -      "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt);
  36.202 +    fun err msg = cat_error msg
  36.203 +      ("The error(s) above occurred in local definition: " ^ string_of_term ctxt eq);
  36.204      val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq)
  36.205        handle TERM _ => err "Not a meta-equality (==)";
  36.206      val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
  36.207 @@ -1282,11 +1276,11 @@
  36.208    | add_case _ (name, NONE) cases = rem_case name cases
  36.209    | add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases;
  36.210  
  36.211 -fun prep_case ctxt name fxs c =
  36.212 +fun prep_case name fxs c =
  36.213    let
  36.214      fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
  36.215        | replace [] ys = ys
  36.216 -      | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
  36.217 +      | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
  36.218      val RuleCases.Case {fixes, assumes, binds, cases} = c;
  36.219      val fixes' = replace fxs fixes;
  36.220      val binds' = map drop_schematic binds;
  36.221 @@ -1294,7 +1288,7 @@
  36.222      if null (fold (Term.add_tvarsT o snd) fixes []) andalso
  36.223        null (fold (fold Term.add_vars o snd) assumes []) then
  36.224          RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
  36.225 -    else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
  36.226 +    else error ("Illegal schematic variable(s) in case " ^ quote name)
  36.227    end;
  36.228  
  36.229  fun fix (x, T) ctxt =
  36.230 @@ -1323,8 +1317,8 @@
  36.231  
  36.232  fun get_case ctxt name xs =
  36.233    (case AList.lookup (op =) (cases_of ctxt) name of
  36.234 -    NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
  36.235 -  | SOME (c, _) => prep_case ctxt name xs c);
  36.236 +    NONE => error ("Unknown case: " ^ quote name)
  36.237 +  | SOME (c, _) => prep_case name xs c);
  36.238  
  36.239  end;
  36.240  
    37.1 --- a/src/Pure/Isar/proof_history.ML	Fri Jan 13 17:39:41 2006 +0100
    37.2 +++ b/src/Pure/Isar/proof_history.ML	Sat Jan 14 17:14:06 2006 +0100
    37.3 @@ -8,7 +8,6 @@
    37.4  signature PROOF_HISTORY =
    37.5  sig
    37.6    type T
    37.7 -  exception FAIL of string
    37.8    val position: T -> int
    37.9    val init: int option -> Proof.state -> T
   37.10    val is_initial: T -> bool
   37.11 @@ -36,8 +35,6 @@
   37.12  
   37.13  datatype T = ProofHistory of proof History.T;
   37.14  
   37.15 -exception FAIL of string;
   37.16 -
   37.17  fun app f (ProofHistory x) = ProofHistory (f x);
   37.18  fun hist_app f = app (History.apply f);
   37.19  
   37.20 @@ -59,7 +56,7 @@
   37.21  
   37.22  val back = hist_app (fn ((_, stq), nodes) =>
   37.23    (case Seq.pull stq of
   37.24 -    NONE => raise FAIL "back: no alternatives"
   37.25 +    NONE => error "back: no alternatives"
   37.26    | SOME result => (result, nodes)));
   37.27  
   37.28  
   37.29 @@ -67,7 +64,7 @@
   37.30  
   37.31  fun applys f = hist_app (fn (node as (st, _), nodes) =>
   37.32    (case Seq.pull (f st) of
   37.33 -    NONE => raise FAIL "empty result sequence -- proof command failed"
   37.34 +    NONE => error "empty result sequence -- proof command failed"
   37.35    | SOME results => (results, node :: nodes)));
   37.36  
   37.37  fun apply f = applys (Seq.single o f);
    38.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Jan 13 17:39:41 2006 +0100
    38.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Jan 14 17:14:06 2006 +0100
    38.3 @@ -179,8 +179,7 @@
    38.4  datatype mfix = Mfix of string * typ * string * int list * int;
    38.5  
    38.6  fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
    38.7 -  error ((if msg = "" then "" else msg ^ "\n") ^
    38.8 -    "in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
    38.9 +  cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   38.10  
   38.11  
   38.12  (* typ_to_nonterm *)
   38.13 @@ -284,7 +283,7 @@
   38.14        | logify_types _ a = a;
   38.15  
   38.16  
   38.17 -    val raw_symbs = read_mixfix sy handle ERROR => err_in_mfix "" mfix;
   38.18 +    val raw_symbs = read_mixfix sy handle ERROR msg => err_in_mfix msg mfix;
   38.19      val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
   38.20      val (const', typ', parse_rules) =
   38.21        if not (exists is_index args) then (const, typ, [])
    39.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Jan 13 17:39:41 2006 +0100
    39.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sat Jan 14 17:14:06 2006 +0100
    39.3 @@ -203,7 +203,7 @@
    39.4  
    39.5  fun the_struct structs i =
    39.6    if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)
    39.7 -  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
    39.8 +  else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
    39.9  
   39.10  fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
   39.11        Lexicon.free (the_struct structs 1)
   39.12 @@ -424,7 +424,7 @@
   39.13  
   39.14  fun the_struct' structs s =
   39.15    [(case Lexicon.read_nat s of
   39.16 -    SOME i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
   39.17 +    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
   39.18    | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
   39.19  
   39.20  fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
    40.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jan 13 17:39:41 2006 +0100
    40.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Jan 14 17:14:06 2006 +0100
    40.3 @@ -447,8 +447,8 @@
    40.4      (case read_asts thy is_logtype syn true root str of
    40.5        [ast] => constify ast
    40.6      | _ => error ("Syntactically ambiguous input: " ^ quote str))
    40.7 -  end handle ERROR =>
    40.8 -    error ("The error(s) above occurred in translation pattern " ^
    40.9 +  end handle ERROR msg =>
   40.10 +    cat_error msg ("The error(s) above occurred in translation pattern " ^
   40.11        quote str);
   40.12  
   40.13  
    41.1 --- a/src/Pure/Thy/thy_info.ML	Fri Jan 13 17:39:41 2006 +0100
    41.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Jan 14 17:14:06 2006 +0100
    41.3 @@ -356,9 +356,10 @@
    41.4          val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict
    41.5            (name :: initiators);
    41.6  
    41.7 -        val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
    41.8 -          error (loader_msg "the error(s) above occurred while examining theory" [name] ^
    41.9 -            (if null initiators then "" else required_by "\n" initiators));
   41.10 +        val (current, (new_deps, parents)) = current_deps ml strict dir name
   41.11 +          handle ERROR msg => cat_error msg
   41.12 +            (loader_msg "the error(s) above occurred while examining theory" [name] ^
   41.13 +              (if null initiators then "" else required_by "\n" initiators));
   41.14          val dir' = if_none (opt_path'' new_deps) dir;
   41.15          val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
   41.16  
    42.1 --- a/src/Pure/axclass.ML	Fri Jan 13 17:39:41 2006 +0100
    42.2 +++ b/src/Pure/axclass.ML	Sat Jan 14 17:14:06 2006 +0100
    42.3 @@ -274,8 +274,8 @@
    42.4      val (c1, c2) = prep_classrel thy raw_cc;
    42.5      val txt = quote (Sign.string_of_classrel thy [c1, c2]);
    42.6      val _ = message ("Proving class inclusion " ^ txt ^ " ...");
    42.7 -    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
    42.8 -      error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
    42.9 +    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   42.10 +      cat_error msg ("The error(s) above occurred while trying to prove " ^ txt);
   42.11    in add_classrel_thms [th] thy end;
   42.12  
   42.13  fun ext_inst_arity prep_arity raw_arity tac thy =
   42.14 @@ -285,9 +285,8 @@
   42.15      val _ = message ("Proving type arity " ^ txt ^ " ...");
   42.16      val props = (mk_arities arity);
   42.17      val ths = Goal.prove_multi thy [] [] props
   42.18 -      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
   42.19 -        handle ERROR_MESSAGE msg =>
   42.20 -          error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   42.21 +      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
   42.22 +        cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt);
   42.23    in add_arity_thms ths thy end;
   42.24  
   42.25  in
    43.1 --- a/src/Pure/context.ML	Fri Jan 13 17:39:41 2006 +0100
    43.2 +++ b/src/Pure/context.ML	Sat Jan 14 17:14:06 2006 +0100
    43.3 @@ -66,7 +66,6 @@
    43.4    val setup: unit -> (theory -> theory) list
    43.5    (*proof context*)
    43.6    type proof
    43.7 -  exception PROOF of string * proof
    43.8    val theory_of_proof: proof -> theory
    43.9    val transfer_proof: theory -> proof -> proof
   43.10    val init_proof: theory -> proof
   43.11 @@ -475,7 +474,7 @@
   43.12  
   43.13  (* use ML text *)
   43.14  
   43.15 -val ml_output = (writeln, error_msg);
   43.16 +val ml_output = (writeln, Output.error_msg);
   43.17  
   43.18  fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
   43.19  
   43.20 @@ -505,15 +504,13 @@
   43.21  
   43.22  datatype proof = Proof of theory_ref * Object.T Inttab.table;
   43.23  
   43.24 -exception PROOF of string * proof;
   43.25 -
   43.26  fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
   43.27  fun data_of_proof (Proof (_, data)) = data;
   43.28  fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
   43.29  
   43.30  fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
   43.31    if not (subthy (deref thy_ref, thy')) then
   43.32 -    raise PROOF ("transfer proof context: no a super theory", prf)
   43.33 +    error "transfer proof context: no a super theory"
   43.34    else Proof (self_ref thy', data);
   43.35  
   43.36  
    44.1 --- a/src/Pure/goal.ML	Fri Jan 13 17:39:41 2006 +0100
    44.2 +++ b/src/Pure/goal.ML	Sat Jan 14 17:14:06 2006 +0100
    44.3 @@ -123,8 +123,8 @@
    44.4      val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
    44.5      val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    44.6  
    44.7 -    fun err msg = raise ERROR_MESSAGE
    44.8 -      (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
    44.9 +    fun err msg = cat_error msg
   44.10 +      ("The error(s) above occurred for the goal statement:\n" ^
   44.11          Sign.string_of_term thy (Term.list_all_free (params, statement)));
   44.12  
   44.13      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
   44.14 @@ -165,7 +165,7 @@
   44.15  fun prove_raw casms cprop tac =
   44.16    (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
   44.17      SOME th => Drule.implies_intr_list casms (finish th)
   44.18 -  | NONE => raise ERROR_MESSAGE "Tactic failed.");
   44.19 +  | NONE => error "Tactic failed.");
   44.20  
   44.21  
   44.22  (* SELECT_GOAL *)
    45.1 --- a/src/Pure/old_goals.ML	Fri Jan 13 17:39:41 2006 +0100
    45.2 +++ b/src/Pure/old_goals.ML	Sat Jan 14 17:14:06 2006 +0100
    45.3 @@ -220,7 +220,7 @@
    45.4     | e => raise e;
    45.5  
    45.6  (*Prints an exception, then fails*)
    45.7 -fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR);
    45.8 +fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR "");
    45.9  
   45.10  (** the prove_goal.... commands
   45.11      Prove theorem using the listed tactics; check it has the specified form.
   45.12 @@ -252,7 +252,7 @@
   45.13  fun prove_goalw thy rths agoal tacsf =
   45.14    let val chorn = read_cterm thy (agoal, propT)
   45.15    in prove_goalw_cterm_general true rths chorn tacsf end
   45.16 -  handle ERROR => error (*from read_cterm?*)
   45.17 +  handle ERROR msg => cat_error msg (*from read_cterm?*)
   45.18                  ("The error(s) above occurred for " ^ quote agoal);
   45.19  
   45.20  (*String version with no meta-rewrite-rules*)
   45.21 @@ -365,7 +365,7 @@
   45.22  (*Version taking the goal as a string*)
   45.23  fun agoalw atomic thy rths agoal =
   45.24      agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
   45.25 -    handle ERROR => error (*from type_assign, etc via prepare_proof*)
   45.26 +    handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
   45.27          ("The error(s) above occurred for " ^ quote agoal);
   45.28  
   45.29  val goalw = agoalw false;
    46.1 --- a/src/Pure/proof_general.ML	Fri Jan 13 17:39:41 2006 +0100
    46.2 +++ b/src/Pure/proof_general.ML	Sat Jan 14 17:14:06 2006 +0100
    46.3 @@ -431,7 +431,7 @@
    46.4    let val name = thy_name file in
    46.5      if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
    46.6       (ThyInfo.touch_child_thys name;
    46.7 -      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
    46.8 +      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
    46.9         (warning msg; warning ("Failed to register theory: " ^ quote name);
   46.10          tell_file_retracted (Path.base (Path.unpack file))))
   46.11      else raise Toplevel.UNDEF
   46.12 @@ -639,7 +639,7 @@
   46.13      in
   46.14          if exists then
   46.15              (issue_pgips [proverinfo]; issue_pgips [File.read path])
   46.16 -        else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   46.17 +        else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   46.18      end;
   46.19  end
   46.20  
   46.21 @@ -1302,9 +1302,9 @@
   46.22                                else false
   46.23             end)
   46.24          | _ => raise PGIP "Invalid PGIP packet received")
   46.25 -     handle (PGIP msg) =>
   46.26 -            (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
   46.27 -                    (XML.string_of_tree xml))))
   46.28 +     handle PGIP msg =>
   46.29 +            error (msg ^ "\nPGIP error occured in XML text below:\n" ^
   46.30 +                    (XML.string_of_tree xml)))
   46.31  
   46.32  val process_pgip = K () o process_pgip_tree o XML.tree_of_string
   46.33  
   46.34 @@ -1336,9 +1336,8 @@
   46.35  and handler (e,srco) =
   46.36      case (e,srco) of
   46.37          (XML_PARSE,SOME src) =>
   46.38 -        panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
   46.39 +        Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
   46.40        | (PGIP_QUIT,_) => ()
   46.41 -      | (ERROR,SOME src) => loop true src (* message already given *)
   46.42        | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
   46.43        | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
   46.44        | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
   46.45 @@ -1441,7 +1440,7 @@
   46.46   (init_setup isar false;
   46.47    if isar then Isar.sync_main () else isa_restart ());
   46.48  
   46.49 -fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode."
   46.50 +fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
   46.51    | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
   46.52  
   46.53  
    47.1 --- a/src/Pure/pure_thy.ML	Fri Jan 13 17:39:41 2006 +0100
    47.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 14 17:14:06 2006 +0100
    47.3 @@ -176,7 +176,7 @@
    47.4  
    47.5  fun name_of_thmref (Name name) = name
    47.6    | name_of_thmref (NameSelection (name, _)) = name
    47.7 -  | name_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
    47.8 +  | name_of_thmref (Fact _) = error "Illegal literal fact";
    47.9  
   47.10  fun map_name_of_thmref f (Name name) = Name (f name)
   47.11    | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
   47.12 @@ -185,7 +185,7 @@
   47.13  fun string_of_thmref (Name name) = name
   47.14    | string_of_thmref (NameSelection (name, is)) =
   47.15        name ^ enclose "(" ")" (commas (map string_of_interval is))
   47.16 -  | string_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
   47.17 +  | string_of_thmref (Fact _) = error "Illegal literal fact";
   47.18  
   47.19  
   47.20  (* select_thm *)
   47.21 @@ -254,7 +254,7 @@
   47.22  (* thms_containing etc. *)
   47.23  
   47.24  fun valid_thms thy (thmref, ths) =
   47.25 -  (case try (transform_error (get_thms thy)) thmref of
   47.26 +  (case try (get_thms thy) thmref of
   47.27      NONE => false
   47.28    | SOME ths' => Thm.eq_thms (ths, ths'));
   47.29  
    48.1 --- a/src/Pure/sign.ML	Fri Jan 13 17:39:41 2006 +0100
    48.2 +++ b/src/Pure/sign.ML	Sat Jan 14 17:14:06 2006 +0100
    48.3 @@ -477,7 +477,7 @@
    48.4      val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
    48.5      val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
    48.6    in cert thy T handle TYPE (msg, _, _) => error msg end
    48.7 -  handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
    48.8 +  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
    48.9  
   48.10  fun gen_read_typ cert (thy, def_sort) str =
   48.11    gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
   48.12 @@ -531,31 +531,29 @@
   48.13      val typs =
   48.14        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   48.15  
   48.16 -    fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   48.17 +    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   48.18          (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   48.19          (intern_sort thy) used freeze typs ts)
   48.20 -      handle TYPE (msg, _, _) => Error msg;
   48.21 +      handle TYPE (msg, _, _) => Exn (ERROR msg);
   48.22  
   48.23      val err_results = map infer termss;
   48.24 -    val errs = List.mapPartial get_error err_results;
   48.25 -    val results = List.mapPartial get_ok err_results;
   48.26 +    val errs = List.mapPartial (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
   48.27 +    val results = List.mapPartial get_result err_results;
   48.28  
   48.29      val ambiguity = length termss;
   48.30 -
   48.31      fun ambig_msg () =
   48.32 -      if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level
   48.33 -      then
   48.34 -        error_msg "Got more than one parse tree.\n\
   48.35 -          \Retry with smaller Syntax.ambiguity_level for more information."
   48.36 -      else ();
   48.37 +      if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then
   48.38 +        "Got more than one parse tree.\n\
   48.39 +        \Retry with smaller Syntax.ambiguity_level for more information."
   48.40 +      else "";
   48.41    in
   48.42 -    if null results then (ambig_msg (); error (cat_lines errs))
   48.43 +    if null results then (cat_error (ambig_msg ()) (cat_lines errs))
   48.44      else if length results = 1 then
   48.45        (if ambiguity > ! Syntax.ambiguity_level then
   48.46          warning "Fortunately, only one parse tree is type correct.\n\
   48.47            \You may still want to disambiguate your grammar or your input."
   48.48        else (); hd results)
   48.49 -    else (ambig_msg (); error ("More than one term is type correct:\n" ^
   48.50 +    else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
   48.51        cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   48.52    end;
   48.53  
   48.54 @@ -578,7 +576,7 @@
   48.55  fun simple_read_term thy T s =
   48.56    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
   48.57    in t end
   48.58 -  handle ERROR => error ("The error(s) above occurred for term " ^ s);
   48.59 +  handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
   48.60  
   48.61  fun read_term thy = simple_read_term thy TypeInfer.logicT;
   48.62  fun read_prop thy = simple_read_term thy propT;
   48.63 @@ -630,7 +628,7 @@
   48.64        val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
   48.65        val a' = Syntax.type_name a mx;
   48.66        val abbr = (a', vs, prep_typ thy rhs)
   48.67 -        handle ERROR => error ("in type abbreviation " ^ quote a');
   48.68 +        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
   48.69        val tsig' = Type.add_abbrevs naming [abbr] tsig;
   48.70      in (naming, syn', tsig', consts) end);
   48.71  
   48.72 @@ -643,7 +641,7 @@
   48.73  fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
   48.74    let
   48.75      fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
   48.76 -      handle ERROR => error ("in arity for type " ^ quote a);
   48.77 +      handle ERROR msg => cat_error msg ("in arity for type " ^ quote a);
   48.78      val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
   48.79    in tsig' end);
   48.80  
   48.81 @@ -655,8 +653,8 @@
   48.82  
   48.83  fun gen_syntax change_gram prep_typ prmode args thy =
   48.84    let
   48.85 -    fun prep (c, T, mx) = (c, prep_typ thy T, mx)
   48.86 -      handle ERROR => error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   48.87 +    fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
   48.88 +      cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   48.89    in thy |> map_syn (change_gram (is_logtype thy) prmode (map prep args)) end;
   48.90  
   48.91  fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
   48.92 @@ -677,7 +675,8 @@
   48.93    let
   48.94      val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
   48.95      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
   48.96 -      handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   48.97 +      handle ERROR msg =>
   48.98 +        cat_error msg ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   48.99      val args = map prep raw_args;
  48.100      val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, T));
  48.101    in
    49.1 --- a/src/Pure/theory.ML	Fri Jan 13 17:39:41 2006 +0100
    49.2 +++ b/src/Pure/theory.ML	Sat Jan 14 17:14:06 2006 +0100
    49.3 @@ -163,8 +163,8 @@
    49.4  
    49.5  (* prepare axioms *)
    49.6  
    49.7 -fun err_in_axm name =
    49.8 -  error ("The error(s) above occurred in axiom " ^ quote name);
    49.9 +fun err_in_axm msg name =
   49.10 +  cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
   49.11  
   49.12  fun no_vars pp tm =
   49.13    (case (Term.term_vars tm, Term.term_tvars tm) of
   49.14 @@ -190,7 +190,7 @@
   49.15      val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
   49.16      val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
   49.17    in cert_axm thy (name, t) end
   49.18 -  handle ERROR => err_in_axm name;
   49.19 +  handle ERROR msg => err_in_axm msg name;
   49.20  
   49.21  fun read_axm thy name_str = read_def_axm (thy, K NONE, K NONE) [] name_str;
   49.22  
   49.23 @@ -199,7 +199,7 @@
   49.24      val pp = Sign.pp thy;
   49.25      val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
   49.26    in (name, no_vars pp t) end
   49.27 -  handle ERROR => err_in_axm name;
   49.28 +  handle ERROR msg => err_in_axm msg name;
   49.29  
   49.30  
   49.31  (* add_axioms(_i) *)
   49.32 @@ -309,7 +309,7 @@
   49.33      defs |> Defs.define (Sign.the_const_type thy)
   49.34        name (prep_const thy const) (map (prep_const thy) rhs_consts)
   49.35    end
   49.36 -  handle ERROR => error (Pretty.string_of (Pretty.block
   49.37 +  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   49.38     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   49.39      Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
   49.40  
    50.1 --- a/src/Sequents/LK/quant.ML	Fri Jan 13 17:39:41 2006 +0100
    50.2 +++ b/src/Sequents/LK/quant.ML	Sat Jan 14 17:14:06 2006 +0100
    50.3 @@ -97,22 +97,22 @@
    50.4  
    50.5  (*INVALID*)
    50.6  goal (theory "LK") "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
    50.7 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
    50.8 +by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
    50.9  (*Check that subgoals remain: proof failed.*)
   50.10  getgoal 1;
   50.11  
   50.12  (*INVALID*)
   50.13  goal (theory "LK") "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
   50.14 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   50.15 +by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
   50.16  getgoal 1;
   50.17  
   50.18  goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
   50.19 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   50.20 +by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
   50.21  (*Check that subgoals remain: proof failed.*)
   50.22  getgoal 1;
   50.23  
   50.24  goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
   50.25 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   50.26 +by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
   50.27  getgoal 1;
   50.28  
   50.29  
    51.1 --- a/src/ZF/Datatype.ML	Fri Jan 13 17:39:41 2006 +0100
    51.2 +++ b/src/ZF/Datatype.ML	Sat Jan 14 17:14:06 2006 +0100
    51.3 @@ -89,7 +89,7 @@
    51.4         val goal = Logic.mk_equals (old, new)
    51.5         val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    51.6             simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
    51.7 -         handle ERROR_MESSAGE msg =>
    51.8 +         handle ERROR msg =>
    51.9           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
   51.10            raise Match)
   51.11     in SOME thm end
    52.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jan 13 17:39:41 2006 +0100
    52.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Jan 14 17:14:06 2006 +0100
    52.3 @@ -35,10 +35,10 @@
    52.4  
    52.5  fun smart_cases thy ss read_prop s =
    52.6    let
    52.7 -    fun err () = error ("Malformed set membership statement: " ^ s);
    52.8 -    val A = read_prop s handle ERROR => err ();
    52.9 +    fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
   52.10 +    val A = read_prop s handle ERROR msg => err msg;
   52.11      val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
   52.12 -      (Logic.strip_imp_concl A)))))) handle TERM _ => err ();
   52.13 +      (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
   52.14    in
   52.15      (case Symtab.lookup (IndCasesData.get thy) c of
   52.16        NONE => error ("Unknown inductive cases rule for set " ^ quote c)
    53.1 --- a/src/ZF/arith_data.ML	Fri Jan 13 17:39:41 2006 +0100
    53.2 +++ b/src/ZF/arith_data.ML	Sat Jan 14 17:14:06 2006 +0100
    53.3 @@ -75,7 +75,7 @@
    53.4        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    53.5          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    53.6    in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
    53.7 -      handle ERROR_MESSAGE msg =>
    53.8 +      handle ERROR msg =>
    53.9          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   53.10    end;
   53.11