# HG changeset patch
# User ballarin
# Date 1228923033 -3600
# Node ID 62dc8762ec005d148613b42f0eca45f4c026bae7
# Parent  df1113d916db73bcdc8f2b6a62da441fdce905f6
Preserve idents (expression in sublocale).

diff -r df1113d916db -r 62dc8762ec00 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 14:45:15 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 16:30:33 2008 +0100
@@ -10,7 +10,6 @@
 
 ML_val {* set new_locales *}
 ML_val {* set Toplevel.debug *}
-ML_val {* set show_hyps *}
 
 
 typedecl int arities int :: "term"
@@ -24,7 +23,7 @@
   int_minus: "(-x) + x = 0"
   int_minus2: "-(-x) = x"
 
-text {* Inference of parameter types *}
+section {* Inference of parameter types *}
 
 locale param1 = fixes p
 print_locale! param1
@@ -44,7 +43,7 @@
 print_locale! param4
 
 
-text {* Incremental type constraints *}
+subsection {* Incremental type constraints *}
 
 locale constraint1 =
   fixes  prod (infixl "**" 65)
@@ -58,7 +57,7 @@
 print_locale! constraint2
 
 
-text {* Inheritance *}
+section {* Inheritance *}
 
 locale semi =
   fixes prod (infixl "**" 65)
@@ -94,7 +93,7 @@
 print_locale! pert_hom' thm pert_hom'_def
 
 
-text {* Syntax declarations *}
+section {* Syntax declarations *}
 
 locale logic =
   fixes land (infixl "&&" 55)
@@ -113,13 +112,13 @@
 print_locale! use_decl thm use_decl_def
 
 
-text {* Foundational versions of theorems *}
+section {* Foundational versions of theorems *}
 
 thm logic.assoc
 thm logic.lor_def
 
 
-text {* Defines *}
+section {* Defines *}
 
 locale logic_def =
   fixes land (infixl "&&" 55)
@@ -149,7 +148,7 @@
 end
 
 
-text {* Notes *}
+section {* Notes *}
 
 (* A somewhat arcane homomorphism example *)
 
@@ -169,7 +168,7 @@
   by (rule semi_hom_mult)
 
 
-text {* Theorem statements *}
+section {* Theorem statements *}
 
 lemma (in lgrp) lcancel:
   "x ** y = x ** z <-> y = z"
@@ -200,7 +199,7 @@
 print_locale! rgrp
 
 
-text {* Patterns *}
+subsection {* Patterns *}
 
 lemma (in rgrp)
   assumes "y ** x = z ** x" (is ?a)
@@ -218,7 +217,7 @@
 qed
 
 
-text {* Interpretation between locales: sublocales *}
+section {* Interpretation between locales: sublocales *}
 
 sublocale lgrp < right: rgrp
 print_facts
@@ -359,7 +358,7 @@
 print_locale! trivial  (* No instance for y created (subsumed). *)
 
 
-text {* Sublocale, then interpretation in theory *}
+subsection {* Sublocale, then interpretation in theory *}
 
 interpretation int: lgrp "op +" "0" "minus"
 proof unfold_locales
@@ -374,7 +373,7 @@
   (* the latter comes through the sublocale relation *)
 
 
-text {* Interpretation in theory, then sublocale *}
+subsection {* Interpretation in theory, then sublocale *}
 
 interpretation (* fol: *) logic "op +" "minus"
 (* FIXME declaration of qualified names *)
@@ -386,10 +385,12 @@
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
 begin
-(* FIXME
+
+(* FIXME interpretation below fails
 definition lor (infixl "||" 50) where
   "x || y = --(-- x && -- y)"
 *)
+
 end
 
 sublocale logic < two: logic2
@@ -398,7 +399,16 @@
 thm two.assoc
 
 
-text {* Interpretation in proofs *}
+subsection {* Declarations and sublocale *}
+
+locale logic_a = logic
+locale logic_b = logic
+
+sublocale logic_a < logic_b
+  by unfold_locales
+
+
+section {* Interpretation in proofs *}
 
 lemma True
 proof
diff -r df1113d916db -r 62dc8762ec00 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Dec 10 14:45:15 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 10 16:30:33 2008 +0100
@@ -410,7 +410,7 @@
 
     val fors = prep_vars fixed context |> fst;
     val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
-    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt);
+    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt);
     val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
 
@@ -484,7 +484,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
-      NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
+      fold NewLocale.activate_local_facts deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
diff -r df1113d916db -r 62dc8762ec00 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Wed Dec 10 14:45:15 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Wed Dec 10 16:30:33 2008 +0100
@@ -47,8 +47,7 @@
   val unfold_attrib: attribute
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
-  (* Identifiers and registrations *)
-  val clear_local_idents: Proof.context -> Proof.context
+  (* Registrations *)
   val add_global_registration: (string * Morphism.morphism) -> theory -> theory
   val get_global_registrations: theory -> (string * Morphism.morphism) list
 
@@ -223,12 +222,10 @@
 fun get_global_idents thy =
   let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
 val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
-val clear_global_idents = put_global_idents empty;
 
 fun get_local_idents ctxt =
   let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
 val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
-val clear_local_idents = put_local_idents empty;
 
 end;