# HG changeset patch
# User wenzelm
# Date 1213305174 -7200
# Node ID 17b63e145986879e323fcc0c782f3a98ba8ece85
# Parent  416d66c36d8f62f9ef104db430801dd9eba89426
use regular error function;

diff -r 416d66c36d8f -r 17b63e145986 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 12 23:12:54 2008 +0200
@@ -236,7 +236,7 @@
                 else F (n+1)
             end
             handle ERROR mesg => F (n+1)
-                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
+                 | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     in
       PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
     end
diff -r 416d66c36d8f -r 17b63e145986 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 23:12:54 2008 +0200
@@ -58,7 +58,7 @@
 
 fun get_dyn_thm thy name atom_name =
   PureThy.get_thm thy name handle ERROR _ =>
-    raise ERROR ("The atom type "^atom_name^" is not defined.");
+    error ("The atom type "^atom_name^" is not defined.");
 
 (* End of function waiting to be in the library :o) *)
 
diff -r 416d66c36d8f -r 17b63e145986 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Jun 12 23:12:54 2008 +0200
@@ -138,7 +138,7 @@
       val data = the (case term_opt of
                         SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
                       | NONE => import_last_fundef (Context.Proof lthy))
-          handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
+          handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt))
 
         val FundefCtxData {termination, R, ...} = data
         val domT = domain_type (fastype_of R)
diff -r 416d66c36d8f -r 17b63e145986 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 12 23:12:54 2008 +0200
@@ -534,8 +534,8 @@
 fun neg_conjecture_clauses st0 n =
   let val st = Seq.hd (neg_skolemize_tac n st0)
       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
-  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
-  handle Option => raise ERROR "unable to Skolemize subgoal";
+  in (neg_clausify (the (metahyps_thms n st)), params) end
+  handle Option => error "unable to Skolemize subgoal";
 
 (*Conversion of a subgoal to conjecture clauses. Each clause has
   leading !!-bound universal variables, to express generality. *)
diff -r 416d66c36d8f -r 17b63e145986 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 23:12:54 2008 +0200
@@ -200,7 +200,7 @@
 
 (*Result of a function type; no need to check that the argument type matches.*)
 fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
-  | result_type _ = raise ERROR "result_type"
+  | result_type _ = error "result_type"
 
 fun type_of_combterm (CombConst(c,tp,_)) = tp
   | type_of_combterm (CombVar(v,tp)) = tp
@@ -235,9 +235,9 @@
       let val c = if c = "equal" then "c_fequal" else c
           val nargs = min_arity_of c
           val args1 = List.take(args, nargs)
-            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
-                                             Int.toString nargs ^ " but is applied to " ^
-                                             space_implode ", " args)
+            handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
+                                         Int.toString nargs ^ " but is applied to " ^
+                                         space_implode ", " args)
           val args2 = List.drop(args, nargs)
           val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
                       else []
@@ -245,7 +245,7 @@
           string_apply (c ^ RC.paren_pack (args1@targs), args2)
       end
   | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
-  | string_of_applic _ = raise ERROR "string_of_applic";
+  | string_of_applic _ = error "string_of_applic";
 
 fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
 
@@ -347,7 +347,7 @@
 
 fun add_clause_decls (Clause {literals, ...}, decls) =
     foldl add_literal_decls decls literals
-    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
+    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
 
 fun decls_of_clauses clauses arity_clauses =
   let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
@@ -360,7 +360,7 @@
 
 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   foldl RC.add_type_sort_preds preds ctypes_sorts
-  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
+  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
 
 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
 fun preds_of_clauses clauses clsrel_clauses arity_clauses =