1.1 --- a/src/Pure/Isar/element.ML	Tue Aug 05 15:07:11 2014 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Aug 05 16:21:27 2014 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4    val satisfy_morphism: witness list -> morphism
     1.5    val eq_morphism: theory -> thm list -> morphism option
     1.6    val init: context_i -> Context.generic -> Context.generic
     1.7 +  val init': context_i -> Context.generic -> Context.generic
     1.8    val activate_i: context_i -> Proof.context -> context_i * Proof.context
     1.9    val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
    1.10  end;
    1.11 @@ -473,18 +474,16 @@
    1.12  
    1.13  (* init *)
    1.14  
    1.15 -local
    1.16 -
    1.17 -fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
    1.18 -  | init0 (Constrains _) = I
    1.19 -  | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
    1.20 +fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
    1.21 +  | init (Constrains _) = I
    1.22 +  | init (Assumes asms) = Context.map_proof (fn ctxt =>
    1.23        let
    1.24          val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
    1.25          val (_, ctxt') = ctxt
    1.26            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    1.27            |> Proof_Context.add_assms_i Assumption.assume_export asms';
    1.28        in ctxt' end)
    1.29 -  | init0 (Defines defs) = Context.map_proof (fn ctxt =>
    1.30 +  | init (Defines defs) = Context.map_proof (fn ctxt =>
    1.31        let
    1.32          val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
    1.33          val asms = defs' |> map (fn (b, (t, ps)) =>
    1.34 @@ -494,17 +493,15 @@
    1.35            |> fold Variable.auto_fixes (map #1 asms)
    1.36            |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
    1.37        in ctxt' end)
    1.38 -  | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
    1.39 +  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
    1.40  
    1.41 -in
    1.42 -
    1.43 -fun init elem context =
    1.44 +fun init' elem context =
    1.45    context
    1.46 -  |> Context.mapping I Thm.unchecked_hyps
    1.47 -  |> init0 elem
    1.48 -  |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
    1.49 -
    1.50 -end;
    1.51 +  |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
    1.52 +  |> init elem
    1.53 +  |> Context.mapping I (fn ctxt =>
    1.54 +      let val ctxt0 = Context.proof_of context
    1.55 +      in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
    1.56  
    1.57  
    1.58  (* activate *)

     2.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 05 15:07:11 2014 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Aug 05 16:21:27 2014 +0200
     2.3 @@ -448,7 +448,7 @@
     2.4    let
     2.5      val thy = Context.theory_of context;
     2.6      val activate =
     2.7 -      activate_notes Element.init
     2.8 +      activate_notes Element.init'
     2.9          (Morphism.transfer_morphism o Context.theory_of) context export;
    2.10    in
    2.11      roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
    2.12 @@ -460,7 +460,7 @@
    2.13      val context = Context.Proof (Proof_Context.init_global thy);
    2.14      val marked = Idents.get context;
    2.15      val (marked', context') = (empty_idents, context)
    2.16 -      |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
    2.17 +      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
    2.18    in
    2.19      context'
    2.20      |> Idents.put (merge_idents (marked, marked'))