tuned msg;
authorwenzelm
Thu Dec 28 14:30:39 2006 +0100 (2006-12-28 ago)
changeset 21919b142e6506469
parent 21918 71e312d6d19a
child 21920 f1c096441023
tuned msg;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Thu Dec 28 14:30:38 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Dec 28 14:30:39 2006 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4    axioms: thm list,
     1.5    params: (string * typ) list,
     1.6    operational: bool (* == at least one class operation,
     1.7 -    or at least two operational superclasses *)};
     1.8 +    or at least two operational superclasses *)}    (* FIXME !? *);
     1.9  
    1.10  type axclasses = axclass Symtab.table * param list;
    1.11  
    1.12 @@ -123,7 +123,7 @@
    1.13  fun get_definition thy c =
    1.14    (case lookup_def thy c of
    1.15      SOME (AxClass info) => info
    1.16 -  | NONE => error ("no such axclass: " ^ quote c));
    1.17 +  | NONE => error ("No such axclass: " ^ quote c));
    1.18  
    1.19  fun class_intros thy =
    1.20    let
    1.21 @@ -146,6 +146,7 @@
    1.22  fun params_of_class thy class =
    1.23    (param_tyvarname, (#params o get_definition thy) class);
    1.24  
    1.25 +
    1.26  (* maintain instances *)
    1.27  
    1.28  val get_instances = #2 o AxClassData.get;
    1.29 @@ -351,6 +352,7 @@
    1.30  
    1.31      (* result *)
    1.32  
    1.33 +    val axclass = make_axclass ((def, intro, axioms), (params_typs, operational));
    1.34      val result_thy =
    1.35        facts_thy
    1.36        |> fold put_classrel (map (pair class) super ~~ classrel)
    1.37 @@ -358,7 +360,7 @@
    1.38        |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
    1.39        |> Sign.restore_naming facts_thy
    1.40        |> map_axclasses (fn (axclasses, parameters) =>
    1.41 -        (Symtab.update (class, make_axclass ((def, intro, axioms), (params_typs, operational))) axclasses,
    1.42 +        (Symtab.update (class, axclass) axclasses,
    1.43            fold (fn x => add_param pp (x, class)) params parameters));
    1.44  
    1.45    in (class, result_thy) end;