# HG changeset patch
# User wenzelm
# Date 972469615 -7200
# Node ID b52d32a114768039a66384863b3a6a11d018715d
# Parent  df38c61bf54132f7cb417262d1ae9fd90e7d3084
antiquotation "goals": error message;

diff -r df38c61bf541 -r b52d32a11476 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue Oct 24 23:38:56 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Wed Oct 25 12:26:55 2000 +0200
@@ -293,7 +293,8 @@
   Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
 
 fun pretty_goals state _ _ =
-  Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state));
+  Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state handle Toplevel.UNDEF =>
+    error "No proof state"));
 
 
 fun output_with pretty src ctxt x =