--- a/src/HOL/Tools/refute.ML Sat Jun 11 22:15:50 2005 +0200
+++ b/src/HOL/Tools/refute.ML Sat Jun 11 22:15:51 2005 +0200
@@ -507,7 +507,7 @@
| _ => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
(* obtain all superclasses of classes in 'sort' *)
(* string list *)
- val superclasses = Graph.all_succs ((#classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
+ val superclasses = Graph.all_succs ((#2 o #classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
in
Library.foldl collect_class_axioms (axs, superclasses)
end
--- a/src/Pure/type_infer.ML Sat Jun 11 22:15:50 2005 +0200
+++ b/src/Pure/type_infer.ML Sat Jun 11 22:15:51 2005 +0200
@@ -523,7 +523,7 @@
val raw_ts' =
map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
val (ts, Ts, unifier) = basic_infer_types pp const_type
- classes arities used freeze is_param raw_ts' pat_Ts';
+ (#2 classes) arities used freeze is_param raw_ts' pat_Ts';
in (ts, unifier) end;
end;