# HG changeset patch
# User haftmann
# Date 1272454197 -7200
# Node ID e741ba542b612c6fa86cb5252c040aa41b8c28fb
# Parent  30f96b4b108b6227a38589b3ebb3506d49172385# Parent  c643b23e8592519aec74a68af8cac86aa88a0a6e
merged

diff -r 30f96b4b108b -r e741ba542b61 NEWS
--- a/NEWS	Wed Apr 28 12:23:14 2010 +0200
+++ b/NEWS	Wed Apr 28 13:29:57 2010 +0200
@@ -84,6 +84,8 @@
 
 *** Pure ***
 
+* Empty class specifications observe default sort.  INCOMPATIBILITY.
+
 * Old 'axclass' has been discontinued.  Use 'class' instead.  INCOMPATIBILITY.
 
 * Code generator: simple concept for abstract datatypes obeying invariants.
diff -r 30f96b4b108b -r e741ba542b61 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Apr 28 12:23:14 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Apr 28 13:29:57 2010 +0200
@@ -100,10 +100,14 @@
 
 (* reading and processing class specifications *)
 
-fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
+fun prep_class_elems prep_decl thy sups raw_elems =
   let
 
     (* user space type system: only permits 'a type variable, improves towards 'a *)
+    val algebra = Sign.classes_of thy;
+    val inter_sort = curry (Sorts.inter_sort algebra);
+    val proto_base_sort = if null sups then Sign.defaultS thy
+      else fold inter_sort (map (base_sort thy) sups) [];
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
         (these_operations thy sups);
@@ -111,17 +115,17 @@
           if v = Name.aT then T
           else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
       | T => T);
-    fun singleton_fixate thy algebra Ts =
+    fun singleton_fixate Ts =
       let
         fun extract f = (fold o fold_atyps) f Ts [];
         val tfrees = extract
           (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
         val inferred_sort = extract
-          (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
+          (fn TVar (_, sort) => inter_sort sort | _ => I);
         val fixate_sort = if null tfrees then inferred_sort
           else case tfrees
            of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
-                then Sorts.inter_sort algebra (a_sort, inferred_sort)
+                then inter_sort a_sort inferred_sort
                 else error ("Type inference imposes additional sort constraint "
                   ^ Syntax.string_of_sort_global thy inferred_sort
                   ^ " of type parameter " ^ Name.aT ^ " of sort "
@@ -136,7 +140,7 @@
     val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
       #> redeclare_operations thy sups
       #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
-      #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
+      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
     val raw_supexpr = (map (fn sup => (sup, (("", false),
       Expression.Positional []))) sups, []);
     val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
@@ -183,11 +187,10 @@
       then error ("Duplicate parameter(s) in superclasses: "
         ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
       else ();
-    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
 
     (* infer types and base sort *)
     val (base_sort, supparam_names, supexpr, inferred_elems) =
-      prep_class_elems thy sups given_basesort raw_elems;
+      prep_class_elems thy sups raw_elems;
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)