# HG changeset patch
# User wenzelm
# Date 1463043429 -7200
# Node ID 5c8e6a751adc7c1846e25dbabf45a1d1ba0926be
# Parent  88474b9fc8440dd3994dd1a4a8da387ce4067749
avoid spurious fact index, notably in "context begin" (via Bundle.context);

diff -r 88474b9fc844 -r 5c8e6a751adc 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