# HG changeset patch
# User ballarin
# Date 1265142200 -3600
# Node ID 87e950efb359d6bba3f00b2b20877c9c5dfa029e
# Parent  8078d496582ce8b591f46282bf08c0052969a352
Clarified invariant; tuned.

diff -r 8078d496582c -r 87e950efb359 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 01 21:59:27 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Feb 02 21:23:20 2010 +0100
@@ -332,9 +332,12 @@
 structure Registrations = Theory_Data
 (
   type T = ((string * (morphism * morphism)) * serial) list *
-    (* registrations, in reverse order of declaration *)
+    (* registrations, in reverse order of declaration;
+       serial points to mixin list *)
     (serial * ((morphism * bool) * serial) list) list;
-    (* alist of mixin lists, per list mixins in reverse order of declaration *)
+    (* alist of mixin lists, per list mixins in reverse order of declaration;
+       lists indexed by registration serial,
+       entries for empty lists may be omitted *)
   val empty = ([], []);
   val extend = I;
   fun merge ((r1, m1), (r2, m2)) : T =
@@ -461,11 +464,10 @@
         fun add_reg (dep', morph') =
           let
             val mixins = collect_mixins thy (dep', morph' $> export);
-            (* FIXME empty list *)
             val serial = serial ();
           in
             Registrations.map (apfst (cons ((dep', (morph', export)), serial))
-              #> apsnd (cons (serial, mixins)))
+              #> not (null mixins) ? apsnd (cons (serial, mixins)))
           end
       in
         (get_idents (Context.Theory thy), thy)