# HG changeset patch
# User wenzelm
# Date 1167409481 -3600
# Node ID 314f9e2a442c895d8c6639545b6d230a0e39082e
# Parent  918fb0fb5c72959c1012ac1c350a75ec6162e974
replaced Sign.classes by Sign.all_classes (topologically sorted);

diff -r 918fb0fb5c72 -r 314f9e2a442c src/HOL/Tools/refute.ML
--- 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  *)
diff -r 918fb0fb5c72 -r 314f9e2a442c src/Pure/Tools/codegen_names.ML
--- 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 =
diff -r 918fb0fb5c72 -r 314f9e2a442c src/Pure/axclass.ML
--- 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;