--- 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
--- 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) *)
--- 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)
--- 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. *)
--- 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 =