src/HOL/Tools/res_hol_clause.ML
changeset 27187 17b63e145986
parent 27178 c8ddb3000743
child 28835 d4d8eba5f781
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 22:41:03 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 23:12:54 2008 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  (*Result of a function type; no need to check that the argument type matches.*)
     1.6  fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
     1.7 -  | result_type _ = raise ERROR "result_type"
     1.8 +  | result_type _ = error "result_type"
     1.9  
    1.10  fun type_of_combterm (CombConst(c,tp,_)) = tp
    1.11    | type_of_combterm (CombVar(v,tp)) = tp
    1.12 @@ -235,9 +235,9 @@
    1.13        let val c = if c = "equal" then "c_fequal" else c
    1.14            val nargs = min_arity_of c
    1.15            val args1 = List.take(args, nargs)
    1.16 -            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
    1.17 -                                             Int.toString nargs ^ " but is applied to " ^
    1.18 -                                             space_implode ", " args)
    1.19 +            handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
    1.20 +                                         Int.toString nargs ^ " but is applied to " ^
    1.21 +                                         space_implode ", " args)
    1.22            val args2 = List.drop(args, nargs)
    1.23            val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
    1.24                        else []
    1.25 @@ -245,7 +245,7 @@
    1.26            string_apply (c ^ RC.paren_pack (args1@targs), args2)
    1.27        end
    1.28    | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
    1.29 -  | string_of_applic _ = raise ERROR "string_of_applic";
    1.30 +  | string_of_applic _ = error "string_of_applic";
    1.31  
    1.32  fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
    1.33  
    1.34 @@ -347,7 +347,7 @@
    1.35  
    1.36  fun add_clause_decls (Clause {literals, ...}, decls) =
    1.37      foldl add_literal_decls decls literals
    1.38 -    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
    1.39 +    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
    1.40  
    1.41  fun decls_of_clauses clauses arity_clauses =
    1.42    let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
    1.43 @@ -360,7 +360,7 @@
    1.44  
    1.45  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
    1.46    foldl RC.add_type_sort_preds preds ctypes_sorts
    1.47 -  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
    1.48 +  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
    1.49  
    1.50  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
    1.51  fun preds_of_clauses clauses clsrel_clauses arity_clauses =