# HG changeset patch
# User wenzelm
# Date 1407248487 -7200
# Node ID 7cf01ece66e4c5347fba305c59e9f4c043e52313
# Parent  0c104888f1caa7510c939b1833383ae31523810d
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;

diff -r 0c104888f1ca -r 7cf01ece66e4 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Aug 05 15:07:11 2014 +0200
+++ b/src/Pure/Isar/element.ML	Tue Aug 05 16:21:27 2014 +0200
@@ -51,6 +51,7 @@
   val satisfy_morphism: witness list -> morphism
   val eq_morphism: theory -> thm list -> morphism option
   val init: context_i -> Context.generic -> Context.generic
+  val init': context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
 end;
@@ -473,18 +474,16 @@
 
 (* init *)
 
-local
-
-fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
-  | init0 (Constrains _) = I
-  | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
+fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
+  | init (Constrains _) = I
+  | init (Assumes asms) = Context.map_proof (fn ctxt =>
       let
         val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
         val (_, ctxt') = ctxt
           |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
           |> Proof_Context.add_assms_i Assumption.assume_export asms';
       in ctxt' end)
-  | init0 (Defines defs) = Context.map_proof (fn ctxt =>
+  | init (Defines defs) = Context.map_proof (fn ctxt =>
       let
         val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
         val asms = defs' |> map (fn (b, (t, ps)) =>
@@ -494,17 +493,15 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
 
-in
-
-fun init elem context =
+fun init' elem context =
   context
-  |> Context.mapping I Thm.unchecked_hyps
-  |> init0 elem
-  |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
-
-end;
+  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
+  |> init elem
+  |> Context.mapping I (fn ctxt =>
+      let val ctxt0 = Context.proof_of context
+      in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
 
 
 (* activate *)
diff -r 0c104888f1ca -r 7cf01ece66e4 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 05 15:07:11 2014 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 05 16:21:27 2014 +0200
@@ -448,7 +448,7 @@
   let
     val thy = Context.theory_of context;
     val activate =
-      activate_notes Element.init
+      activate_notes Element.init'
         (Morphism.transfer_morphism o Context.theory_of) context export;
   in
     roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
@@ -460,7 +460,7 @@
     val context = Context.Proof (Proof_Context.init_global thy);
     val marked = Idents.get context;
     val (marked', context') = (empty_idents, context)
-      |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
+      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
   in
     context'
     |> Idents.put (merge_idents (marked, marked'))