use regular error function;
authorwenzelm
Thu Jun 12 23:12:54 2008 +0200 (2008-06-12)
changeset 2718717b63e145986
parent 27186 416d66c36d8f
child 27188 e47b069cab35
use regular error function;
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jun 12 22:41:03 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 12 23:12:54 2008 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4                  else F (n+1)
     1.5              end
     1.6              handle ERROR mesg => F (n+1)
     1.7 -                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     1.8 +                 | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     1.9      in
    1.10        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    1.11      end
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 22:41:03 2008 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 23:12:54 2008 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4  
     2.5  fun get_dyn_thm thy name atom_name =
     2.6    PureThy.get_thm thy name handle ERROR _ =>
     2.7 -    raise ERROR ("The atom type "^atom_name^" is not defined.");
     2.8 +    error ("The atom type "^atom_name^" is not defined.");
     2.9  
    2.10  (* End of function waiting to be in the library :o) *)
    2.11  
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Jun 12 22:41:03 2008 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Jun 12 23:12:54 2008 +0200
     3.3 @@ -138,7 +138,7 @@
     3.4        val data = the (case term_opt of
     3.5                          SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
     3.6                        | NONE => import_last_fundef (Context.Proof lthy))
     3.7 -          handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
     3.8 +          handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt))
     3.9  
    3.10          val FundefCtxData {termination, R, ...} = data
    3.11          val domT = domain_type (fastype_of R)
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jun 12 22:41:03 2008 +0200
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 12 23:12:54 2008 +0200
     4.3 @@ -534,8 +534,8 @@
     4.4  fun neg_conjecture_clauses st0 n =
     4.5    let val st = Seq.hd (neg_skolemize_tac n st0)
     4.6        val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
     4.7 -  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
     4.8 -  handle Option => raise ERROR "unable to Skolemize subgoal";
     4.9 +  in (neg_clausify (the (metahyps_thms n st)), params) end
    4.10 +  handle Option => error "unable to Skolemize subgoal";
    4.11  
    4.12  (*Conversion of a subgoal to conjecture clauses. Each clause has
    4.13    leading !!-bound universal variables, to express generality. *)
     5.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 22:41:03 2008 +0200
     5.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 23:12:54 2008 +0200
     5.3 @@ -200,7 +200,7 @@
     5.4  
     5.5  (*Result of a function type; no need to check that the argument type matches.*)
     5.6  fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
     5.7 -  | result_type _ = raise ERROR "result_type"
     5.8 +  | result_type _ = error "result_type"
     5.9  
    5.10  fun type_of_combterm (CombConst(c,tp,_)) = tp
    5.11    | type_of_combterm (CombVar(v,tp)) = tp
    5.12 @@ -235,9 +235,9 @@
    5.13        let val c = if c = "equal" then "c_fequal" else c
    5.14            val nargs = min_arity_of c
    5.15            val args1 = List.take(args, nargs)
    5.16 -            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
    5.17 -                                             Int.toString nargs ^ " but is applied to " ^
    5.18 -                                             space_implode ", " args)
    5.19 +            handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
    5.20 +                                         Int.toString nargs ^ " but is applied to " ^
    5.21 +                                         space_implode ", " args)
    5.22            val args2 = List.drop(args, nargs)
    5.23            val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
    5.24                        else []
    5.25 @@ -245,7 +245,7 @@
    5.26            string_apply (c ^ RC.paren_pack (args1@targs), args2)
    5.27        end
    5.28    | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
    5.29 -  | string_of_applic _ = raise ERROR "string_of_applic";
    5.30 +  | string_of_applic _ = error "string_of_applic";
    5.31  
    5.32  fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
    5.33  
    5.34 @@ -347,7 +347,7 @@
    5.35  
    5.36  fun add_clause_decls (Clause {literals, ...}, decls) =
    5.37      foldl add_literal_decls decls literals
    5.38 -    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
    5.39 +    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
    5.40  
    5.41  fun decls_of_clauses clauses arity_clauses =
    5.42    let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
    5.43 @@ -360,7 +360,7 @@
    5.44  
    5.45  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
    5.46    foldl RC.add_type_sort_preds preds ctypes_sorts
    5.47 -  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
    5.48 +  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
    5.49  
    5.50  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
    5.51  fun preds_of_clauses clauses clsrel_clauses arity_clauses =