Fix issue related to mixins in roundup.
Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Mar 25 15:18:44 2013 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Mar 25 19:53:44 2013 +0100
@@ -757,6 +757,14 @@
 lemma "0 = glob_one (op +)" by (rule int.def.one_def)
 lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
 
+text {* Roundup applies mixins at declaration level in DFS tree *}
+
+locale roundup = fixes x assumes true: "x <-> True"
+
+sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True"
+  apply unfold_locales apply (simp add: true) done
+lemma (in roundup) "True & True <-> True" by (rule sub.true)
+
 
 section {* Interpretation in proofs *}
 

--- a/src/Pure/Isar/locale.ML	Mon Mar 25 15:18:44 2013 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 25 19:53:44 2013 +0100
@@ -259,7 +259,7 @@
 
 val roundup_bound = 120;
 
-fun add thy depth stem export (name, morph, mixins) (deps, marked) =
+fun add thy depth stem export (name, morph) (deps, marked) =
   if depth > roundup_bound
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   else
@@ -269,17 +269,16 @@
       if redundant_ident thy marked (name, instance) then (deps, marked)
       else
         let
-          val full_morph = morph $> compose_mixins mixins $> stem;
           (* no inheritance of mixins, regardless of requests by clients *)
           val dependencies = dependencies_of thy name |>
             map (fn ((name', (morph', export')), serial') =>
-              (name', morph' $> export', mixins_of thy name serial'));
+              (name', morph' $> export' $> compose_mixins (mixins_of thy name serial')));
           val marked' = insert_idents (name, instance) marked;
           val (deps', marked'') =
-            fold_rev (add thy (depth + 1) full_morph export) dependencies
+            fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies
               ([], marked');
         in
-          ((name, full_morph) :: deps' @ deps, marked'')
+          ((name, morph $> stem) :: deps' @ deps, marked'')
         end
     end;
 
@@ -293,7 +292,7 @@
     (* Find all dependencies including new ones (which are dependencies enriching
       existing registrations). *)
     val (dependencies, marked') =
-      add thy 0 Morphism.identity export (name, morph, []) ([], empty_idents);
+      add thy 0 Morphism.identity export (name, morph) ([], empty_idents);
     (* Filter out fragments from marked; these won't be activated. *)
     val dependencies' = filter_out (fn (name, morph) =>
       redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies;