Clarified invariant; tuned.
authorballarin
Tue Feb 02 21:23:20 2010 +0100 (2010-02-02)
changeset 3609087e950efb359
parent 36089 8078d496582c
child 36091 055934ed89b0
Clarified invariant; tuned.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Feb 01 21:59:27 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Feb 02 21:23:20 2010 +0100
     1.3 @@ -332,9 +332,12 @@
     1.4  structure Registrations = Theory_Data
     1.5  (
     1.6    type T = ((string * (morphism * morphism)) * serial) list *
     1.7 -    (* registrations, in reverse order of declaration *)
     1.8 +    (* registrations, in reverse order of declaration;
     1.9 +       serial points to mixin list *)
    1.10      (serial * ((morphism * bool) * serial) list) list;
    1.11 -    (* alist of mixin lists, per list mixins in reverse order of declaration *)
    1.12 +    (* alist of mixin lists, per list mixins in reverse order of declaration;
    1.13 +       lists indexed by registration serial,
    1.14 +       entries for empty lists may be omitted *)
    1.15    val empty = ([], []);
    1.16    val extend = I;
    1.17    fun merge ((r1, m1), (r2, m2)) : T =
    1.18 @@ -461,11 +464,10 @@
    1.19          fun add_reg (dep', morph') =
    1.20            let
    1.21              val mixins = collect_mixins thy (dep', morph' $> export);
    1.22 -            (* FIXME empty list *)
    1.23              val serial = serial ();
    1.24            in
    1.25              Registrations.map (apfst (cons ((dep', (morph', export)), serial))
    1.26 -              #> apsnd (cons (serial, mixins)))
    1.27 +              #> not (null mixins) ? apsnd (cons (serial, mixins)))
    1.28            end
    1.29        in
    1.30          (get_idents (Context.Theory thy), thy)