--- a/src/HOL/Tools/refute.ML Fri Dec 29 16:47:49 2006 +0100
+++ b/src/HOL/Tools/refute.ML Fri Dec 29 17:24:41 2006 +0100
@@ -424,7 +424,7 @@
val rec_names = Symtab.fold (append o #rec_names o snd)
(DatatypePackage.get_datatypes thy) [];
(* string list *)
- val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
+ val const_of_class_names = map Logic.const_of_class (Sign.all_classes thy)
(* given a constant 's' of type 'T', which is a subterm of 't', where *)
(* 't' has a (possibly) more general type, the schematic type *)
(* variables in 't' are instantiated to match the type 'T' (may raise *)
--- a/src/Pure/Tools/codegen_names.ML Fri Dec 29 16:47:49 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML Fri Dec 29 17:24:41 2006 +0100
@@ -154,7 +154,7 @@
| NONE => error (errmsg x) end;
fun thyname_of_class thy =
- thyname_of thy (fn thy => member (op =) (Sign.classes thy))
+ thyname_of thy (fn thy => member (op =) (Sign.all_classes thy))
(fn class => "thyname_of_class: no such class: " ^ quote class);
fun thyname_of_classrel thy =
--- a/src/Pure/axclass.ML Fri Dec 29 16:47:49 2006 +0100
+++ b/src/Pure/axclass.ML Fri Dec 29 17:24:41 2006 +0100
@@ -126,7 +126,7 @@
let
fun add_intro c =
(case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
- val classes = Sign.classes thy;
+ val classes = Sign.all_classes thy;
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;