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