1.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 30 21:23:04 2012 +0200
     1.3 @@ -362,10 +362,7 @@
     1.4  fun stable_command exec =
     1.5    (case Exn.capture Command.memo_result exec of
     1.6      Exn.Exn exn => not (Exn.is_interrupt exn)
     1.7 -  | Exn.Res ((st, _), _) =>
     1.8 -      (case try Toplevel.theory_of st of
     1.9 -        NONE => true
    1.10 -      | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
    1.11 +  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
    1.12  
    1.13  fun make_required nodes =
    1.14    let