changeset 49011 | 9c68e43502ce |
parent 49010 | 72808e956879 |
child 49012 | 8686c36fa27d |
--- a/src/Pure/PIDE/document.ML Thu Aug 30 16:39:50 2012 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 30 19:18:49 2012 +0200 @@ -357,7 +357,7 @@ is_some (Exn.get_res (Exn.capture (fn () => fst (fst (Command.memo_result (the (get_result node)))) |> Toplevel.end_theory Position.none - |> Thm.join_all_proofs) ())); + |> Thm.join_theory_proofs) ())); fun stable_command exec = (case Exn.capture Command.memo_result exec of