# HG changeset patch
# User ballarin
# Date 1364237624 -3600
# Node ID c3eb0b517ced0f71cecbba53fd04733d944bd8d8
# Parent  9bed72e554750062dc51fc3f96d9ccd1aa4305a1
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.

diff -r 9bed72e55475 -r c3eb0b517ced src/FOL/ex/Locale_Test/Locale_Test1.thy
--- 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 *}
 
diff -r 9bed72e55475 -r c3eb0b517ced src/Pure/Isar/locale.ML
--- 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;