# HG changeset patch # User wenzelm # Date 1118520951 -7200 # Node ID 6ff17d08c3d5597019ac57e24d70fd6d15337845 # Parent 838c65dad23a17ede4488825c92ef2bddea170ea accomodate changed #classes; diff -r 838c65dad23a -r 6ff17d08c3d5 src/HOL/Tools/refute.ML --- 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 diff -r 838c65dad23a -r 6ff17d08c3d5 src/Pure/type_infer.ML --- 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;