src/HOL/Tools/refute.ML
changeset 15794 5de27a5fc5ed
parent 15783 82e40c9a0f3f
child 16050 828fc32f390f
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Apr 21 18:56:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Apr 21 18:57:18 2005 +0200
     1.3 @@ -448,8 +448,8 @@
     1.4  		in
     1.5  			map_term_types
     1.6  				(map_type_tvar
     1.7 -					(fn (v,_) =>
     1.8 -						case Vartab.lookup (typeSubs, v) of
     1.9 +					(fn v =>
    1.10 +						case Type.lookup (typeSubs, v) of
    1.11  						  NONE =>
    1.12  							(* schematic type variable not instantiated *)
    1.13  							raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
    1.14 @@ -459,11 +459,11 @@
    1.15  		end
    1.16  		(* applies a type substitution 'typeSubs' for all type variables in a  *)
    1.17  		(* term 't'                                                            *)
    1.18 -		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
    1.19 +		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
    1.20  		fun monomorphic_term typeSubs t =
    1.21  			map_term_types (map_type_tvar
    1.22 -				(fn (v, _) =>
    1.23 -					case Vartab.lookup (typeSubs, v) of
    1.24 +				(fn v =>
    1.25 +					case Type.lookup (typeSubs, v) of
    1.26  					  NONE =>
    1.27  						(* schematic type variable not instantiated *)
    1.28  						raise ERROR
    1.29 @@ -483,11 +483,11 @@
    1.30  						(* (string * Term.term) list *)
    1.31  						val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.32  							let
    1.33 -								val (idx, _) = (case term_tvars ax of
    1.34 +								val (idx, S) = (case term_tvars ax of
    1.35  									  [is] => is
    1.36  									| _    => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable"))
    1.37  							in
    1.38 -								(axname, monomorphic_term (Vartab.make [(idx, T)]) ax)
    1.39 +								(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
    1.40  							end) class_axioms
    1.41  						(* Term.term list * (string * Term.term) list -> Term.term list *)
    1.42  						fun collect_axiom (axs, (axname, ax)) =