src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Thu Dec 28 14:30:38 2006 +0100
+++ b/src/Pure/axclass.ML	Thu Dec 28 14:30:39 2006 +0100
@@ -70,7 +70,7 @@
   axioms: thm list,
   params: (string * typ) list,
   operational: bool (* == at least one class operation,
-    or at least two operational superclasses *)};
+    or at least two operational superclasses *)}    (* FIXME !? *);
 
 type axclasses = axclass Symtab.table * param list;
 
@@ -123,7 +123,7 @@
 fun get_definition thy c =
   (case lookup_def thy c of
     SOME (AxClass info) => info
-  | NONE => error ("no such axclass: " ^ quote c));
+  | NONE => error ("No such axclass: " ^ quote c));
 
 fun class_intros thy =
   let
@@ -146,6 +146,7 @@
 fun params_of_class thy class =
   (param_tyvarname, (#params o get_definition thy) class);
 
+
 (* maintain instances *)
 
 val get_instances = #2 o AxClassData.get;
@@ -351,6 +352,7 @@
 
     (* result *)
 
+    val axclass = make_axclass ((def, intro, axioms), (params_typs, operational));
     val result_thy =
       facts_thy
       |> fold put_classrel (map (pair class) super ~~ classrel)
@@ -358,7 +360,7 @@
       |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
       |> Sign.restore_naming facts_thy
       |> map_axclasses (fn (axclasses, parameters) =>
-        (Symtab.update (class, make_axclass ((def, intro, axioms), (params_typs, operational))) axclasses,
+        (Symtab.update (class, axclass) axclasses,
           fold (fn x => add_param pp (x, class)) params parameters));
 
   in (class, result_thy) end;