src/HOL/Tools/refute.ML
changeset 18678 dd0c569fa43d
parent 17493 cf8713d880b1
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -466,7 +466,7 @@
     1.4  					case Type.lookup (typeSubs, v) of
     1.5  					  NONE =>
     1.6  						(* schematic type variable not instantiated *)
     1.7 -						raise ERROR
     1.8 +						error ""
     1.9  					| SOME typ =>
    1.10  						typ)) t
    1.11  		(* Term.term list * Term.typ -> Term.term list *)
    1.12 @@ -550,7 +550,7 @@
    1.13  							| NONE =>
    1.14  								get_typedefn axms
    1.15  						end
    1.16 -						handle ERROR           => get_typedefn axms
    1.17 +						handle ERROR _         => get_typedefn axms
    1.18  						     | MATCH           => get_typedefn axms
    1.19  						     | Type.TYPE_MATCH => get_typedefn axms)
    1.20  				in
    1.21 @@ -650,7 +650,7 @@
    1.22  							else
    1.23  								get_defn axms
    1.24  						end
    1.25 -						handle ERROR           => get_defn axms
    1.26 +						handle ERROR _         => get_defn axms
    1.27  						     | TERM _          => get_defn axms
    1.28  						     | Type.TYPE_MATCH => get_defn axms)
    1.29  					(* axiomatic type classes *)