--- 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;