--- a/src/HOL/Tools/refute.ML Thu Apr 21 18:56:03 2005 +0200
+++ b/src/HOL/Tools/refute.ML Thu Apr 21 18:57:18 2005 +0200
@@ -448,8 +448,8 @@
in
map_term_types
(map_type_tvar
- (fn (v,_) =>
- case Vartab.lookup (typeSubs, v) of
+ (fn v =>
+ case Type.lookup (typeSubs, v) of
NONE =>
(* schematic type variable not instantiated *)
raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
@@ -459,11 +459,11 @@
end
(* applies a type substitution 'typeSubs' for all type variables in a *)
(* term 't' *)
- (* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
+ (* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
fun monomorphic_term typeSubs t =
map_term_types (map_type_tvar
- (fn (v, _) =>
- case Vartab.lookup (typeSubs, v) of
+ (fn v =>
+ case Type.lookup (typeSubs, v) of
NONE =>
(* schematic type variable not instantiated *)
raise ERROR
@@ -483,11 +483,11 @@
(* (string * Term.term) list *)
val monomorphic_class_axioms = map (fn (axname, ax) =>
let
- val (idx, _) = (case term_tvars ax of
+ val (idx, S) = (case term_tvars ax of
[is] => is
| _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable"))
in
- (axname, monomorphic_term (Vartab.make [(idx, T)]) ax)
+ (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
end) class_axioms
(* Term.term list * (string * Term.term) list -> Term.term list *)
fun collect_axiom (axs, (axname, ax)) =