fixed reading of class specs: declare class operations in context

--- a/src/Pure/Isar/class.ML	Mon Jan 26 22:14:18 2009 +0100
+++ b/src/Pure/Isar/class.ML	Mon Jan 26 22:14:19 2009 +0100
@@ -91,20 +91,32 @@
 
   in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
 
+val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
+      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 =
+  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);
+    val fixate_sort = if null tfrees then inferred_sort
+      else let val a_sort = (snd o the_single) tfrees
+      in if Sorts.sort_le algebra (a_sort, inferred_sort)
+        then Sorts.inter_sort algebra (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 "
+          ^ Syntax.string_of_sort_global thy a_sort)
+      end
+  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));
 
-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) =>
-      if v = Name.aT then T
-      else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification"));
-
-val singleton_fixate = (map o map_atyps) (fn TVar (vi, sort)
-  => TFree (Name.aT, sort) | T => T);
-
 fun add_tfrees_of_element (Element.Fixes fxs) = fold (fn (_, SOME T, _) => Term.add_tfreesT T
       | _ => I) fxs
   | add_tfrees_of_element (Element.Constrains cnstrs) = fold (Term.add_tfreesT o snd) cnstrs
@@ -142,8 +154,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
-      |> add_typ_check ~2 "singleton_fixate" singleton_fixate
+      |> 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))
       |> prep_decl supexpr raw_elems;
     (*FIXME check for *all* side conditions here, extra check function for elements,
       less side-condition checks in check phase*)

--- a/src/Pure/Isar/class_target.ML	Mon Jan 26 22:14:18 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Mon Jan 26 22:14:19 2009 +0100
@@ -29,6 +29,7 @@
     -> (string * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
+  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
 
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
@@ -298,6 +299,10 @@
 fun these_unchecks thy =
   map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
 
+fun redeclare_const thy c =
+  let val b = Sign.base_name c
+  in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
+
 fun synchronize_class_syntax sort base_sort ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -308,9 +313,6 @@
       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
     val secondary_constraints =
       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
-    fun declare_const (c, _) =
-      let val b = Sign.base_name c
-      in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
     fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
      of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
          of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
@@ -326,7 +328,7 @@
     val unchecks = these_unchecks thy sort;
   in
     ctxt
-    |> fold declare_const primary_constraints
+    |> fold (redeclare_const thy o fst) primary_constraints
     |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
         (((improve, subst), true), unchecks)), false))
     |> Overloading.set_primary_constraints
@@ -338,6 +340,9 @@
     val base_sort = base_sort thy class;
   in synchronize_class_syntax [class] base_sort ctxt end;
 
+fun redeclare_operations thy sort =
+  fold (redeclare_const thy o fst) (these_operations thy sort);
+
 fun begin sort base_sort ctxt =
   ctxt
   |> Variable.declare_term
@@ -489,7 +494,8 @@
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
     val params = these_params thy sort;
-    fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco)
+    fun get_param tyco (param, (_, (c, ty))) =
+      if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
     val inst_params = map_product get_param tycos params |> map_filter I;