Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
antiquotation "goals": error message;
authorwenzelm
Wed, 25 Oct 2000 12:26:55 +0200
changeset 10323 b52d32a11476
parent 10322 df38c61bf541
child 10324 498999fd7c37
antiquotation "goals": error message;
src/Pure/Isar/isar_output.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle