accomodate changed #classes;
authorwenzelm
Sat Jun 11 22:15:51 2005 +0200 (2005-06-11 ago)
changeset 163666ff17d08c3d5
parent 16365 838c65dad23a
child 16367 e11031fe4096
accomodate changed #classes;
src/HOL/Tools/refute.ML
src/Pure/type_infer.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Jun 11 22:15:50 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Jun 11 22:15:51 2005 +0200
     1.3 @@ -507,7 +507,7 @@
     1.4  					| _               => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
     1.5  				(* obtain all superclasses of classes in 'sort' *)
     1.6  				(* string list *)
     1.7 -				val superclasses = Graph.all_succs ((#classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
     1.8 +				val superclasses = Graph.all_succs ((#2 o #classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
     1.9  			in
    1.10  				Library.foldl collect_class_axioms (axs, superclasses)
    1.11  			end
     2.1 --- a/src/Pure/type_infer.ML	Sat Jun 11 22:15:50 2005 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Sat Jun 11 22:15:51 2005 +0200
     2.3 @@ -523,7 +523,7 @@
     2.4      val raw_ts' =
     2.5        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
     2.6      val (ts, Ts, unifier) = basic_infer_types pp const_type
     2.7 -      classes arities used freeze is_param raw_ts' pat_Ts';
     2.8 +      (#2 classes) arities used freeze is_param raw_ts' pat_Ts';
     2.9    in (ts, unifier) end;
    2.10  
    2.11  end;