src/Pure/Isar/expression.ML

 fun prep_statement prep activate raw_elems raw_stmt ctxt =
   let
     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
 
 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;

     val ctxt' = ctxt
       |> fix_params fixed
       |> 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
 
 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;