# HG changeset patch
# User ballarin
# Date 1254423138 -7200
# Node ID 88b58880d52c978964734315bdfc52da36c98d4b
# Parent  29941e925c82f6b7d1b1b5909cc68084a63e7378# Parent  3a2fa964ad08d34311ff9b8c5ffa15a3f032da45
Merged.

diff -r 3a2fa964ad08 -r 88b58880d52c NEWS
--- a/NEWS	Thu Oct 01 20:20:56 2009 +0200
+++ b/NEWS	Thu Oct 01 20:52:18 2009 +0200
@@ -15,6 +15,14 @@
 * On instantiation of classes, remaining undefined class parameters
 are formally declared.  INCOMPATIBILITY.
 
+* Locale interpretation propagates mixins along the locale hierarchy.
+The currently only available mixins are the equations used to map
+local definitions to terms of the target domain of an interpretation.
+
+* Reactivated diagnositc command 'print_interps'.  Use 'print_interps l'
+to print all interpretations of locale l in the theory.  Interpretations
+in proofs are not shown.
+
 
 *** HOL ***
 
diff -r 3a2fa964ad08 -r 88b58880d52c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Oct 01 20:20:56 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Oct 01 20:52:18 2009 +0200
@@ -820,7 +820,8 @@
       #-> (fn eqns => fold (fn ((dep, morph), wits) =>
         fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
             (map (Element.morph_witness export') wits))
-          (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
+          (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
+          export thy) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
diff -r 3a2fa964ad08 -r 88b58880d52c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Oct 01 20:20:56 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Oct 01 20:52:18 2009 +0200
@@ -68,8 +68,10 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
-  val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
+  val add_registration: string * morphism -> (morphism * bool) option ->
+    morphism -> theory -> theory
+  val amend_registration: string * morphism -> morphism * bool ->
+    morphism -> theory -> theory
   val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
@@ -474,7 +476,8 @@
         |> roundup thy add_reg export (name, base_morph)
         |> snd
         (* add mixin *)
-        |> amend_registration (name, base_morph) mixin export
+        |> (case mixin of NONE => I
+             | SOME mixin => amend_registration (name, base_morph) mixin export)
         (* activate import hierarchy as far as not already active *)
         |> Context.theory_map (activate_facts' export (name, base_morph))
       end