src/Pure/PIDE/document.ML
changeset 49012 8686c36fa27d
parent 49011 9c68e43502ce
child 49061 7449b804073b
--- a/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 30 21:23:04 2012 +0200
@@ -362,10 +362,7 @@
 fun stable_command exec =
   (case Exn.capture Command.memo_result exec of
     Exn.Exn exn => not (Exn.is_interrupt exn)
-  | Exn.Res ((st, _), _) =>
-      (case try Toplevel.theory_of st of
-        NONE => true
-      | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
+  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
 
 fun make_required nodes =
   let