no base sort in class import

--- a/NEWS	Wed Jan 21 18:37:44 2009 +0100
+++ b/NEWS	Wed Jan 21 23:40:23 2009 +0100
@@ -66,6 +66,12 @@
 
 *** Pure ***
 
+* Class declaration: sc. "base sort" must not be given in import list
+any longer but is inferred from the specification.  Particularly in HOL,
+write
+
+    class foo = ...     instead of      class foo = type + ...
+
 * Type Binding.T gradually replaces formerly used type bstring for names
 to be bound.  Name space interface for declarations has been simplified:
 

--- a/src/HOL/HOL.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -208,34 +208,34 @@
 
 subsubsection {* Generic classes and algebraic operations *}
 
-class default = type +
+class default =
   fixes default :: 'a
 
-class zero = type + 
+class zero = 
   fixes zero :: 'a  ("0")
 
-class one = type +
+class one =
   fixes one  :: 'a  ("1")
 
 hide (open) const zero one
 
-class plus = type +
+class plus =
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
 
-class minus = type +
+class minus =
   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
 
-class uminus = type +
+class uminus =
   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
 
-class times = type +
+class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
-class inverse = type +
+class inverse =
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
 
-class abs = type +
+class abs =
   fixes abs :: "'a \<Rightarrow> 'a"
 begin
 
@@ -247,10 +247,10 @@
 
 end
 
-class sgn = type +
+class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
 
-class ord = type +
+class ord =
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
@@ -1675,7 +1675,7 @@
 
 text {* Equality *}
 
-class eq = type +
+class eq =
   fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
 begin

--- a/src/HOL/Int.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Int.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -599,7 +599,7 @@
   Bit1 :: "int \<Rightarrow> int" where
   [code del]: "Bit1 k = 1 + k + k"
 
-class number = type + -- {* for numeric types: nat, int, real, \dots *}
+class number = -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
 use "Tools/numeral.ML"

--- a/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -32,7 +32,7 @@
   with the oracle.  
 *}
 
-class ml_equiv = type
+class ml_equiv
 
 text {*
   Instances of @{text "ml_equiv"} should only be declared for those types,

--- a/src/HOL/Library/Quotient.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Library/Quotient.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -21,7 +21,7 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-class eqv = type +
+class eqv =
   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
 
 class equiv = eqv +

--- a/src/HOL/Nat.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -1515,7 +1515,7 @@
 
 subsection {* size of a datatype value *}
 
-class size = type +
+class size =
   fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
 
 end

--- a/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -49,7 +49,7 @@
 
 text {* free type variables *}
 
-class ftv = type +
+class ftv =
   fixes ftv :: "'a \<Rightarrow> tvar list"
 
 instantiation * :: (ftv, ftv) ftv

--- a/src/HOL/Parity.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Parity.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -8,7 +8,7 @@
 imports Plain Presburger
 begin
 
-class even_odd = type + 
+class even_odd = 
   fixes even :: "'a \<Rightarrow> bool"
 
 abbreviation

--- a/src/HOL/Power.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Power.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -11,7 +11,7 @@
 imports Nat
 begin
 
-class power = type +
+class power =
   fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
 
 subsection{*Powers for Arbitrary Monoids*}

--- a/src/HOL/RealVector.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/RealVector.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -124,7 +124,7 @@
 
 subsection {* Real vector spaces *}
 
-class scaleR = type +
+class scaleR =
   fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
 begin
 
@@ -418,7 +418,7 @@
 
 subsection {* Real normed vector spaces *}
 
-class norm = type +
+class norm =
   fixes norm :: "'a \<Rightarrow> real"
 
 instantiation real :: norm

--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -11,7 +11,7 @@
 
 text {* A type class of kleene algebras *}
 
-class star = type +
+class star =
   fixes star :: "'a \<Rightarrow> 'a"
 
 class idem_add = ab_semigroup_add +

--- a/src/HOL/Typedef.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Typedef.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -123,7 +123,7 @@
 text {* This class is just a workaround for classes without parameters;
   it shall disappear as soon as possible. *}
 
-class itself = type + 
+class itself = 
   fixes itself :: "'a itself"
 
 setup {*

--- a/src/HOL/Word/BitSyntax.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Word/BitSyntax.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -12,7 +12,7 @@
 imports BinGeneral
 begin
 
-class bit = type +
+class bit =
   fixes bitNOT :: "'a \<Rightarrow> 'a"       ("NOT _" [70] 71)
     and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
     and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)

--- a/src/HOL/Word/Size.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Word/Size.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -18,7 +18,7 @@
   some duplication with the definitions in @{text "Numeral_Type"}.
 *}
 
-class len0 = type +
+class len0 =
   fixes len_of :: "'a itself \<Rightarrow> nat"
 
 text {* 

--- a/src/HOLCF/Porder.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOLCF/Porder.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -10,7 +10,7 @@
 
 subsection {* Type class for partial orders *}
 
-class sq_ord = type +
+class sq_ord =
   fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 notation

--- a/src/Pure/Isar/class.ML	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/Pure/Isar/class.ML	Wed Jan 21 23:40:23 2009 +0100
@@ -92,8 +92,8 @@
 fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
   let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
 
-fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
-      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
+val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
+      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
       else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
         (*FIXME does not occur*)
   | T as TFree (v, sort) =>
@@ -119,11 +119,12 @@
   let
     (* prepare import *)
     val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val (sups, others_basesort) = map (prep_class thy) raw_supclasses
-      |> Sign.minimize_sort thy
-      |> List.partition (is_class thy);
-
-    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+    val sups = map (prep_class thy) raw_supclasses
+      |> Sign.minimize_sort thy;
+    val _ = case filter_out (is_class thy) sups
+     of [] => ()
+      | no_classes => error ("These are not classes: " ^ commas (map quote no_classes));
+          val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
     val supparam_names = map fst supparams;
     val _ = if has_duplicates (op =) supparam_names
       then error ("Duplicate parameter(s) in superclasses: "
@@ -131,7 +132,7 @@
       else ();
     val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
       sups, []);
-    val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
+    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
 
     (* infer types and base sort *)
     val base_constraints = (map o apsnd)
@@ -139,10 +140,9 @@
         (these_operations thy sups);
     val ((_, _, inferred_elems), _) = ProofContext.init thy
       |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
-      |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
+      |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
       |> add_typ_check ~2 "singleton_fixate" singleton_fixate
       |> prep_decl supexpr raw_elems;
-    (*FIXME propagation of given base sort into class spec broken*)
     (*FIXME check for *all* side conditions here, extra check function for elements,
       less side-condition checks in check phase*)
     val base_sort = if null inferred_elems then given_basesort else
@@ -170,45 +170,6 @@
 val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
 val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
 
-(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
-  let
-    (*FIXME 2009 simplify*)
-    val supclasses = map (prep_class thy) raw_supclasses;
-    val supsort = Sign.minimize_sort thy supclasses;
-    val (sups, bases) = List.partition (is_class thy) supsort;
-    val base_sort = if null sups then supsort else
-      Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
-        (map (base_sort thy) sups, bases);
-    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
-    val supparam_names = map fst supparams;
-    val _ = if has_duplicates (op =) supparam_names
-      then error ("Duplicate parameter(s) in superclasses: "
-        ^ (commas o map quote o duplicates (op =)) supparam_names)
-      else ();
-
-    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
-      sups, []);
-    val constrain = Element.Constrains ((map o apsnd o map_atyps)
-      (K (TFree (Name.aT, base_sort))) supparams);
-      (*FIXME 2009 perhaps better: control type variable by explicit
-      parameter instantiation of import expression*)
-    val begin_ctxt = begin sups base_sort
-      #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
-          (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
-            should constraints be issued in begin?*)
-    val ((_, _, syntax_elems), _) = ProofContext.init thy
-      |> begin_ctxt
-      |> process_decl supexpr raw_elems;
-    fun fork_syn (Element.Fixes xs) =
-          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
-          #>> Element.Fixes
-      | fork_syn x = pair x;
-    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
-  in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
-
-val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
-val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
-
 fun add_consts bname class base_sort sups supparams global_syntax thy =
   let
     (*FIXME 2009 simplify*)