diff -r 6dd8866eca69 -r d11d11da0d90 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun May 11 20:23:08 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Mon May 12 12:01:02 2014 +0200
@@ -194,6 +194,21 @@
 
 local
 
+fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
+  let
+    val name = Toplevel.name_of tr;
+    val res =
+      if Keyword.is_theory name andalso not (Keyword.is_theory_begin name) then
+        Toplevel.reset_theory st0
+      else if Keyword.is_proof name then
+        Toplevel.reset_proof st0
+      else NONE;
+  in
+    (case res of
+      NONE => st0
+    | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
+  end) ();
+
 fun run int tr st =
   if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
@@ -220,14 +235,16 @@
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
+fun eval_state span tr ({malformed, state, ...}: eval_state) =
   if malformed then
     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   else
     let
-      val malformed' = Toplevel.is_malformed tr;
+      val _ = Multithreading.interrupted ();
 
-      val _ = Multithreading.interrupted ();
+      val malformed' = Toplevel.is_malformed tr;
+      val st = reset_state tr state;
+
       val _ = status tr Markup.running;
       val (errs1, result) = run true tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');