--- 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 *)