src/Pure/Isar/toplevel.ML
changeset 60895 501be4aa75b4
parent 60693 044f8bb3dd30
child 61208 19118f9b939d
--- a/src/Pure/Isar/toplevel.ML	Tue Aug 11 17:06:23 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Aug 11 18:00:28 2015 +0200
@@ -582,7 +582,9 @@
 
 fun transition int tr st =
   let
-    val (st', opt_err) = app int tr st;
+    val (st', opt_err) =
+      Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st)
+        (fn () => app int tr st) ();
     val opt_err' = opt_err |> Option.map
       (fn Runtime.EXCURSION_FAIL exn_info => exn_info
         | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));