# HG changeset patch
# User haftmann
# Date 1157350648 -7200
# Node ID 95f6d354b0edc6ef4861bac0601450a5e92254f9
# Parent  2b3fc1459ffa519c72f00a787372988f89ffed40
proper project_sort

diff -r 2b3fc1459ffa -r 95f6d354b0ed src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sat Sep 02 03:10:27 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon Sep 04 08:17:28 2006 +0200
@@ -29,7 +29,7 @@
   val certify_sort: theory -> sort -> sort
   val read_class: theory -> xstring -> class
   val read_sort: theory -> string -> sort
-  val operational_algebra: theory -> Sorts.algebra * (sort -> sort)
+  val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   val the_consts_sign: theory -> class -> string * (string * typ) list
   val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
   val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
diff -r 2b3fc1459ffa -r 95f6d354b0ed src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Sep 02 03:10:27 2006 +0200
+++ b/src/Pure/sorts.ML	Mon Sep 04 08:17:28 2006 +0200
@@ -43,7 +43,7 @@
   val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
   val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
-  val project_algebra: Pretty.pp -> (class -> bool) -> algebra -> algebra * (sort -> sort)
+  val project_algebra: Pretty.pp -> (class -> bool) -> algebra -> (sort -> sort) * algebra
   type class_error
   val class_error: Pretty.pp -> class_error -> 'a
   exception CLASS_ERROR of class_error
@@ -57,7 +57,7 @@
   val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
 end;
 
-structure Sorts (*: SORTS *) =
+structure Sorts : SORTS =
 struct
 
 
@@ -281,21 +281,13 @@
 
 fun project_algebra pp proj (algebra as Algebra {classes, arities}) =
   let
+    val proj_sort = norm_sort algebra o filter proj o Graph.all_succs classes;
+    fun proj_arity (c, (_, Ss)) =
+      if proj c then SOME (c, (c, map proj_sort Ss)) else NONE;
     val classes' = classes |> Graph.project proj;
-    val proj' = can (Graph.get_node classes');
-    fun proj_classes class =
-      if proj' class
-      then [class]
-      else (norm_sort algebra o maps proj_classes o super_classes algebra) class;
-    val class_subst = fold (fn class => Symtab.update (class, proj_classes class))
-      (Graph.keys classes) Symtab.empty;
-    fun proj_arity (c, (_, Ss)) =
-      if proj' c then SOME (c,
-        (c, map (norm_sort algebra o filter proj' o Graph.all_succs classes) Ss)) else NONE;
     val arities' = arities |> (Symtab.map o map_filter) proj_arity;
-    val algebra' = rebuild_arities pp (make_algebra (classes', arities'));
-    val proj_sort = norm_sort algebra' o maps (the o Symtab.lookup class_subst);
-  in (rebuild_arities pp (make_algebra (classes', arities')), proj_sort) end;
+  in (proj_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
+
 
 
 (** sorts of types **)