avoid spurious fact index, notably in "context begin" (via Bundle.context);
authorwenzelm
Thu, 12 May 2016 10:57:09 +0200
changeset 63086 5c8e6a751adc
parent 63085 88474b9fc844
child 63087 be252979cfe5
avoid spurious fact index, notably in "context begin" (via Bundle.context);
src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 12 10:21:59 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 12 10:57:09 2016 +0200
@@ -444,9 +444,10 @@
     val ((_, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
         ([], []) I raw_elems raw_stmt ctxt;
-    val (_, ctxt') = ctxt
+    val ctxt' = ctxt
       |> Proof_Context.set_stmt true
-      |> fold_map activate elems;
+      |> fold_map activate elems |> #2
+      |> Proof_Context.restore_stmt ctxt;
   in (concl, ctxt') end;
 
 in
@@ -475,7 +476,8 @@
       |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
     val (elems', ctxt'') = ctxt'
       |> Proof_Context.set_stmt true
-      |> fold_map activate elems;
+      |> fold_map activate elems
+      ||> Proof_Context.restore_stmt ctxt';
   in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
 
 in