--- a/src/Pure/Isar/proof.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 11 22:55:47 2011 +0200
@@ -1008,8 +1008,8 @@
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
|> int ? (fn goal_state =>
(case test_proof goal_state of
- Exn.Result (SOME _) => goal_state
- | Exn.Result NONE => error (fail_msg (context_of goal_state))
+ Exn.Res (SOME _) => goal_state
+ | Exn.Res NONE => error (fail_msg (context_of goal_state))
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;