# HG changeset patch
# User wenzelm
# Date 1190832633 -7200
# Node ID c25aa6ae64ec409994e91ee9207f1742b3f5c8e7
# Parent  a87d8d31abc0b6ab385c80c714a5ddb044305b13
Sign.minimize/complete_sort;

diff -r a87d8d31abc0 -r c25aa6ae64ec src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 26 20:27:58 2007 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 26 20:50:33 2007 +0200
@@ -255,8 +255,6 @@
      of [] => ()
       | dupl_tycos => error ("type constructors occur more than once in arities: "
           ^ (commas o map quote) dupl_tycos);
-    val super_sort =
-      (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory;
     fun get_consts_class tyco ty class =
       let
         val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
@@ -268,7 +266,7 @@
       let
         val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
           (Name.names Name.context "'a" asorts))
-      in maps (get_consts_class tyco ty) (super_sort sort) end;
+      in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
     val cs = maps get_consts_sort arities;
     fun mk_typnorm thy (ty, ty_sc) =
       case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
@@ -418,7 +416,7 @@
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
-        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
+        (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
       Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
         o these o Option.map #params o try (AxClass.get_definition thy)) class,
@@ -575,8 +573,8 @@
       | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
     val supclasses = map (prep_class thy) raw_supclasses;
     val sups = filter (is_some o lookup_class_data thy) supclasses
-      |> Sign.certify_sort thy;
-    val supsort = Sign.certify_sort thy supclasses;
+      |> Sign.minimize_sort thy;
+    val supsort = Sign.minimize_sort thy supclasses;
     val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
     val supexpr = Locale.Merge (suplocales @ includes);
     val supparams = (map fst o Locale.parameters_of_expr thy)
@@ -721,8 +719,7 @@
     val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
     fun prove_classrel (class, superclass) thy =
       let
-        val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
-              o Sign.classes_of) thy [superclass]
+        val classes = Sign.complete_sort thy [superclass]
           |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
         fun instance_subclass (class1, class2) thy  =
           let
@@ -731,7 +728,7 @@
             val intro = #intro (AxClass.get_definition thy class2)
               |> Drule.instantiate' [SOME (Thm.ctyp_of thy
                   (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
-            val thm = 
+            val thm =
               intro
               |> OF_LAST (interp OF ax)
               |> strip_all_ofclass thy (Sign.super_classes thy class2);
diff -r a87d8d31abc0 -r c25aa6ae64ec src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Sep 26 20:27:58 2007 +0200
+++ b/src/Pure/Isar/code.ML	Wed Sep 26 20:50:33 2007 +0200
@@ -541,7 +541,7 @@
 
 fun weakest_constraints thy (class, tyco) =
   let
-    val all_superclasses = class :: Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class];
+    val all_superclasses = Sign.complete_sort thy [class];
   in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    of SOME sorts => sorts
     | NONE => Sign.arity_sorts thy tyco [class]
@@ -555,7 +555,7 @@
   in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    of SOME sorts => sorts
     | NONE => replicate
-        (Sign.arity_number thy tyco) (Sign.certify_sort thy (Sign.all_classes thy))
+        (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
   end;
 
 fun gen_classop_typ constr thy class (c, tyco) = 
diff -r a87d8d31abc0 -r c25aa6ae64ec src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Sep 26 20:27:58 2007 +0200
+++ b/src/Pure/axclass.ML	Wed Sep 26 20:50:33 2007 +0200
@@ -225,7 +225,7 @@
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
-    val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err ();
+    val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
@@ -291,7 +291,7 @@
 
     val bconst = Logic.const_of_class bclass;
     val class = Sign.full_name thy bclass;
-    val super = Sign.certify_sort thy raw_super;
+    val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
 
     fun prep_axiom t =
       (case Term.add_tfrees t [] of
@@ -420,7 +420,7 @@
 fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   let
     val class = Sign.full_name thy bclass;
-    val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
+    val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
   in
     thy
     |> Sign.primitive_class (bclass, super)