# HG changeset patch
# User haftmann
# Date 1234981113 -3600
# Node ID aee7610106fd26d9e2e629b0562c4666ee5838ee
# Parent  68331b62c87310373c578f54fc3a5eb34d8f1007
sort instances wrt. to class hierarchy

diff -r 68331b62c873 -r aee7610106fd src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Feb 18 19:18:33 2009 +0100
+++ b/src/Pure/sorts.ML	Wed Feb 18 19:18:33 2009 +0100
@@ -302,11 +302,21 @@
 
 (* algebra projections *)
 
-fun classrels_of (Algebra {classes, ...}) =
-  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
+val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
+
+fun classrels_of algebra = 
+  map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
 
-fun instances_of (Algebra {arities, ...}) =
-  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
+fun instances_of algebra =
+  let
+    val arities = arities_of algebra;
+    val all_classes = sorted_classes algebra;
+    fun sort_classes cs = filter (member (op = o apsnd fst) cs)
+      all_classes;
+  in
+    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
+      arities []
+  end;
 
 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let
diff -r 68331b62c873 -r aee7610106fd src/Tools/code/code_funcgr_new.ML
--- a/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 19:18:33 2009 +0100
+++ b/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 19:18:33 2009 +0100
@@ -205,16 +205,6 @@
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;
 
-fun instances_of (*FIXME move to sorts.ML*) algebra =
-  let
-    val { classes, arities } = Sorts.rep_algebra algebra;
-    val sort_classes = fn cs => filter (member (op = o apsnd fst) cs)
-      (flat (rev (Graph.strong_conn classes)));
-  in
-    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
-      arities []
-  end;
-
 fun algebra_of thy vardeps =
   let
     val pp = Syntax.pp_global thy;
@@ -223,7 +213,7 @@
     val classrels = Sorts.classrels_of thy_algebra
       |> filter (is_proper o fst)
       |> (map o apsnd) (filter is_proper);
-    val instances = instances_of thy_algebra
+    val instances = Sorts.instances_of thy_algebra
       |> filter (is_proper o snd);
     fun add_class (class, superclasses) algebra =
       Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;