diff -r 0cec730b3942 -r 1cad5c2b2a0b src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Dec 27 15:24:23 2005 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Dec 27 15:24:40 2005 +0100
@@ -7,7 +7,11 @@
 
 signature CLASS_PACKAGE =
 sig
-  val add_classentry: class -> string list -> string list -> theory -> theory
+  val add_class: bstring -> Locale.expr -> Element.context list -> theory
+    -> ProofContext.context * theory
+  val add_class_i: bstring -> Locale.expr -> Element.context_i list -> theory
+    -> ProofContext.context * theory
+  val add_classentry: class -> xstring list -> xstring list -> theory -> theory
   val the_consts: theory -> class -> string list
   val the_tycos: theory -> class -> (string * string) list
 
@@ -65,6 +69,8 @@
   ClassesData.map (apfst (Symtab.update (class, data)));
 fun add_const class const =
   ClassesData.map (apsnd (Symtab.update (const, class)));
+val the_consts = #consts oo get_class_data;
+val the_tycos = #tycos oo get_class_data;
 
 
 (* name mangling *)
@@ -76,67 +82,91 @@
   #axclass_name (get_class_data thy class);
 
 
-(* assign consts to type classes *)
+(* classes *)
 
 local
 
-fun gen_add_consts prep_class prep_const (raw_class, raw_consts_new) thy =
+open Element
+
+fun gen_add_class add_locale bname raw_import raw_body thy =
   let
-    val class = prep_class thy raw_class;
-    val consts_new = map (prep_const thy) raw_consts_new;
-    val {locale_name, axclass_name, consts, tycos} =
-      get_class_data thy class;
+    fun extract_notes_consts thy elems =
+      elems
+      |> List.mapPartial
+           (fn (Notes notes) => SOME notes
+             | _ => NONE)
+      |> Library.flat
+      |> map (fn (_, facts) => map fst facts)
+      |> Library.flat o Library.flat
+      |> map prop_of
+      |> (fn ts => fold (curry add_term_consts) ts [])
+      |> tap (writeln o commas);
+    fun extract_tyvar_name thy tys =
+      fold (curry add_typ_tfrees) tys []
+      |> (fn [(v, [])] => v
+           | [(v, sort)] =>
+                if Sorts.sort_eq (Sign.classes_of thy) (Sign.defaultS thy, sort)
+                then v 
+                else error ("sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
+           | [] => error ("no class type variable")
+           | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
+    fun extract_tyvar_consts thy elems =
+      elems
+      |> List.mapPartial
+           (fn (Fixes consts) => SOME consts
+             | _ => NONE)
+      |> Library.flat
+      |> map (fn (c, ty, syn) => ((c, the ty), the syn))
+      |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts));
+    (* fun remove_local_syntax ((c, ty), _) thy =
+      thy
+      |> Sign.add_syntax_i [(c, ty, Syntax.NoSyn)]; *)
+    fun add_global_const ((c, ty), syn) thy =
+      thy
+      |> Sign.add_consts_i [(c, ty, syn)]
+      |> `(fn thy => Sign.intern_const thy c)
+    fun add_axclass bname_axiom locale_pred cs thy =
+      thy
+      |> AxClass.add_axclass_i (bname, Sign.defaultS thy)
+           [Thm.no_attributes (bname_axiom,
+              Const (ObjectLogic.judgment_name thy, dummyT) $
+                list_comb (Const (locale_pred, dummyT), map (fn c => Const (c, dummyT)) cs)
+              |> curry (inferT_axm thy) "locale_pred" |> snd)]
+      |-> (fn _ => `(fn thy => Sign.intern_class thy bname))
+    fun print_ctxt ctxt elem = 
+      map Pretty.writeln (Element.pretty_ctxt ctxt elem)
   in
     thy
-    |> put_class_data class {
-         locale_name = locale_name,
-         axclass_name = axclass_name,
-         consts = consts @ consts_new,
-         tycos = tycos
-       }
-    |> fold (add_const class) consts_new
+    |> add_locale bname raw_import raw_body
+    |-> (fn (elems : context_i list, ctxt) =>
+       tap (fn _ => map (print_ctxt ctxt) elems)
+    #> tap (fn thy => extract_notes_consts thy elems)
+    #> `(fn thy => Locale.intern thy bname)
+    #-> (fn name_locale =>
+       `(fn thy => extract_tyvar_consts thy elems)
+    #-> (fn (v, consts) =>
+       fold_map add_global_const consts
+    #-> (fn cs =>
+       add_axclass (bname ^ "_intro") name_locale cs
+    #-> (fn name_axclass =>
+       put_class_data name_locale {
+          locale_name = name_locale,
+          axclass_name = name_axclass,
+          consts = cs,
+          tycos = []
+        })
+    #> fold (add_const name_locale) cs
+    #> pair ctxt
+    ))))
   end;
 
 in
 
-val add_consts = gen_add_consts Sign.intern_class Sign.intern_const;
-val add_consts_i = gen_add_consts (K I) (K I);
+val add_class = gen_add_class (Locale.add_locale_context true);
+val add_class_i = gen_add_class (Locale.add_locale_context_i true);
 
 end; (* local *)
 
-val the_consts = #consts oo get_class_data;
-
-
-(* assign type constructors to type classes *)
-
-local
-
-fun gen_add_tycos prep_class prep_type (raw_class, raw_tycos_new) thy =
-  let
-    val class = prep_class thy raw_class
-    val tycos_new = map (prep_type thy) raw_tycos_new
-    val {locale_name, axclass_name, consts, tycos} =
-      get_class_data thy class
-  in
-    thy
-    |> put_class_data class {
-         locale_name = locale_name,
-         axclass_name = axclass_name,
-         consts = consts,
-         tycos = tycos @ tycos_new
-       }
-  end;
-
-in
-
-fun add_tycos xs thy =
-  gen_add_tycos Sign.intern_class (rpair (Context.theory_name thy) oo Sign.intern_type) xs thy;
-val add_tycos_i = gen_add_tycos (K I) (K I);
-
-end; (* local *)
-
-val the_tycos = #tycos oo get_class_data;
-
 
 (* class queries *)
 
@@ -156,12 +186,16 @@
   end;
 
 fun get_arities thy sort tycon =
-  Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort
+  Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort)
   |> map (syntactic_sort_of thy);
 
 fun get_superclasses thy class =
-  Sorts.superclasses (Sign.classes_of thy) class
-  |> syntactic_sort_of thy;
+  if is_class thy class
+  then
+    Sorts.superclasses (Sign.classes_of thy) class
+    |> syntactic_sort_of thy
+  else
+    error ("no syntactic class: " ^ class);
 
 
 (* instance queries *)
@@ -227,7 +261,8 @@
       ) subclasses;
     fun mk_class_deriv thy subclasses superclass =
       case get_superclass_derivation (subclasses, superclass)
-      of (subclass::deriv) => ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses);
+      of (subclass::deriv) =>
+        ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses);
     fun mk_lookup (sort_def, (Type (tycon, tys))) =
           let
             val arity_lookup = map2 (curry mk_lookup)
@@ -236,7 +271,7 @@
       | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
           let
             fun mk_look class =
-              let val (deriv, classindex) = mk_class_deriv thy sort_use class
+              let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class
               in Lookup (deriv, (vname, classindex)) end;
           in map mk_look sort_def end;
   in
@@ -250,21 +285,49 @@
 
 (* intermediate auxiliary *)
 
-fun add_classentry raw_class raw_consts raw_tycos thy =
+fun add_classentry raw_class raw_cs raw_tycos thy =
   let
     val class = Sign.intern_class thy raw_class;
+    val cs = map (Sign.intern_const thy) raw_cs;
+    val tycos = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_tycos;
   in
     thy
     |> put_class_data class {
          locale_name = "",
          axclass_name = class,
-         consts = [],
-         tycos = []
+         consts = cs,
+         tycos = tycos
        }
-    |> add_consts (class, raw_consts)
-    |> add_tycos (class, raw_tycos)
+    |> fold (add_const class) cs
   end;
-  
+
+
+(* toplevel interface *)
+
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+in
+
+val classK = "class_class"
+
+val locale_val =
+  (P.locale_expr --
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
+  Scan.repeat1 P.context_element >> pair Locale.empty);
+
+val classP =
+  OuterSyntax.command classK "operational type classes" K.thy_decl
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
+      >> (Toplevel.theory_context
+          o (fn f => swap o f) o (fn (name, (expr, elems)) => add_class name expr elems)));
+
+val _ = OuterSyntax.add_parsers [classP];
+
+end; (* local *)
+
 
 (* setup *)