src/Pure/Isar/class.ML

   in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
 
 
 (* reading and processing class specifications *)
 
-fun prep_class_elems prep_decl thy supexpr sups proto_base_sort raw_elems =
+fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
   let
 
     (* user space type system: only permits 'a type variable, improves towards 'a *)
     val base_constraints = (map o apsnd)
       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)

                   ^ Syntax.string_of_sort_global thy inferred_sort
                   ^ " of type parameter " ^ Name.aT ^ " of sort "
                   ^ Syntax.string_of_sort_global thy a_sort ^ ".")
             | _ => error "Multiple type variables in class specification.";
       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
-    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));
-
-    (* preprocessing elements, retrieving base sort from type-checked elements *)
+    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));
+
+    (* preprocessing elements, retrieving base sort from typechecked elements *)
     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));
-    val ((_, _, inferred_elems), _) = ProofContext.init thy
-      |> prep_decl supexpr init_class_body raw_elems;
+    val raw_supexpr = (map (fn sup => (sup, (("", false),
+      Expression.Positional []))) sups, []);
+    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
+      |> prep_decl raw_supexpr init_class_body raw_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
           fold_types f t #> (fold o fold_types) f ts) o snd) assms
       | fold_element_types f (Element.Defines _) =

           error ("\"notes\" element not allowed in class specification.");
     val base_sort = if null inferred_elems then proto_base_sort else
       case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
        of [] => error "No type variable in class specification"
         | [(_, sort)] => sort
-        | _ => error "Multiple type variables in class specification"
-
-  in (base_sort, inferred_elems) end;
+        | _ => error "Multiple type variables in class specification";
+    val supparams = map (fn ((c, T), _) =>
+      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
+    val supparam_names = map fst supparams;
+    fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
+    val supexpr = (map (fn sup => (sup, (("", false),
+      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
+        map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
+
+  in (base_sort, supparam_names, supexpr, inferred_elems) end;
 
 val cert_class_elems = prep_class_elems Expression.cert_declaration;
 val read_class_elems = prep_class_elems Expression.cert_read_declaration;
 
 fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =

     val sups = map (prep_class thy) raw_supclasses
       |> Sign.minimize_sort thy;
     val _ = case filter_out (is_class thy) sups
      of [] => ()
       | no_classes => error ("No (proper) 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
+    val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+    val raw_supparam_names = map fst raw_supparams;
+    val _ = if has_duplicates (op =) raw_supparam_names
       then error ("Duplicate parameter(s) in superclasses: "
-        ^ (commas o map quote o duplicates (op =)) supparam_names)
+        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
       else ();
-    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
-      sups, []);
     val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
 
     (* infer types and base sort *)
-    val (base_sort, inferred_elems) = prep_class_elems thy supexpr sups
-      given_basesort raw_elems;
-    val sup_sort = inter_sort base_sort sups
+    val (base_sort, supparam_names, supexpr, inferred_elems) =
+      prep_class_elems thy sups given_basesort raw_elems;
+    val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = begin sups base_sort (ProofContext.init thy)
+    val class_ctxt = begin sups base_sort (ProofContext.init thy);
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
       then error ("No type variable in part of specification element "
         ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))

           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
-      (K (TFree (Name.aT, base_sort))) supparams);
+      (K (TFree (Name.aT, base_sort))) raw_supparams);
       (*FIXME perhaps better: control type variable by explicit
       parameter instantiation of import expression*)
 
-  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
+  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), ((*constrain :: *)elems, global_syntax)) end;
 
 val cert_class_spec = prep_class_spec (K I) cert_class_elems;
 val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
 
 
 (* class establishment *)
 
-fun add_consts class base_sort sups supparams global_syntax thy =
+fun add_consts class base_sort sups supparam_names global_syntax thy =
   let
     (*FIXME simplify*)
-    val supconsts = supparams
+    val supconsts = supparam_names
       |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     val all_params = Locale.params_of thy class;
-    val raw_params = (snd o chop (length supparams)) all_params;
+    val raw_params = (snd o chop (length supparam_names)) all_params;
     fun add_const ((raw_c, raw_ty), _) thy =
       let
         val b = Binding.name raw_c;
         val c = Sign.full_name thy b;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;

     |> fold_map add_const raw_params
     ||> Sign.restore_naming thy
     |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   end;
 
-fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
+fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
   let
     (*FIXME simplify*)
     fun globalize param_map = map_aterms
       (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
         | t => t);

     fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
      of [] => NONE
       | [thm] => SOME thm;
   in
     thy
-    |> add_consts class base_sort sups supparams global_syntax
+    |> add_consts class base_sort sups supparam_names global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
           [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy bname;
-    val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
-      prep_spec thy raw_supclasses raw_elems;
+    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
+      prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
     |> Expression.add_locale bname Binding.empty supexpr elems
     |> snd |> LocalTheory.exit_global
-    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
+    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
        Locale.add_registration_eqs (class, base_morph) eqs export_morph