# HG changeset patch
# User wenzelm
# Date 1519053857 -3600
# Node ID 189c68964ab28b5d08bc456e2768e3d6b33b9444
# Parent  23659b5dde1dd3bdc476d6ff1bcb89dfec22e9e1
clarified modules;

diff -r 23659b5dde1d -r 189c68964ab2 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Feb 19 15:46:10 2018 +0100
+++ b/src/Pure/Isar/element.ML	Mon Feb 19 16:24:17 2018 +0100
@@ -51,7 +51,6 @@
   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;
@@ -502,14 +501,6 @@
       in ctxt' end)
   | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
 
-fun init' elem context =
-  context
-  |> 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 23659b5dde1d -r 189c68964ab2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 19 15:46:10 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 16:24:17 2018 +0100
@@ -409,6 +409,14 @@
 
 (* Declarations, facts and entire locale content *)
 
+fun init_element elem context =
+  context
+  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
+  |> Element.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);
+
 fun activate_syntax_decls (name, morph) context =
   let
     val thy = Context.theory_of context;
@@ -460,7 +468,7 @@
   |> Context_Position.set_visible_generic false
   |> pair (Idents.get context)
   |> roundup (Context.theory_of context)
-      (activate_notes Element.init' Morphism.transfer_morphism'' context export)
+      (activate_notes init_element Morphism.transfer_morphism'' context export)
       (the_default Morphism.identity export) dep
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;
@@ -481,7 +489,7 @@
     context
     |> Context_Position.set_visible_generic false
     |> pair empty_idents
-    |> activate_all name thy Element.init' Morphism.transfer_morphism''
+    |> activate_all name thy init_element Morphism.transfer_morphism''
     |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
     |> Context_Position.restore_visible_generic context
     |> Context.proof_of