src/Pure/sorts.ML

   val add_class: Pretty.pp -> class * class list -> algebra -> algebra
   val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
   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
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool

      variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
 end;
 
-structure Sorts (*: SORTS *) =
+structure Sorts : SORTS =
 struct
 
 
 (** ordered lists of sorts **)
 

       |> add_arities_table pp algebra0 arities2;
   in make_algebra (classes', arities') end;
 
 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 **)
 
 (* errors *)