--- a/src/HOL/Tools/refute.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/Tools/refute.ML Sat Jan 14 17:14:06 2006 +0100
@@ -466,7 +466,7 @@
case Type.lookup (typeSubs, v) of
NONE =>
(* schematic type variable not instantiated *)
- raise ERROR
+ error ""
| SOME typ =>
typ)) t
(* Term.term list * Term.typ -> Term.term list *)
@@ -550,7 +550,7 @@
| NONE =>
get_typedefn axms
end
- handle ERROR => get_typedefn axms
+ handle ERROR _ => get_typedefn axms
| MATCH => get_typedefn axms
| Type.TYPE_MATCH => get_typedefn axms)
in
@@ -650,7 +650,7 @@
else
get_defn axms
end
- handle ERROR => get_defn axms
+ handle ERROR _ => get_defn axms
| TERM _ => get_defn axms
| Type.TYPE_MATCH => get_defn axms)
(* axiomatic type classes *)