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