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.
Now catches the error of calling tgoalw when there are no goals to prove,
authorpaulson
Fri, 04 Jul 1997 12:32:31 +0200
changeset 3497 122e80826c95
parent 3496 32e7edc609fd
child 3498 807549666b9c
Now catches the error of calling tgoalw when there are no goals to prove, instead of just letting USyntax.list_mk_conj raise an exception
TFL/post.sml file | annotate | diff | comparison | revisions 
--- a/TFL/post.sml	Fri Jul 04 12:31:20 1997 +0200
+++ b/TFL/post.sml	Fri Jul 04 12:32:31 1997 +0200
@@ -53,11 +53,11 @@
  * puts them into a goalstack.
  *--------------------------------------------------------------------------*)
 fun tgoalw thy defs rules = 
-   let val L = termination_goals rules
-       open USyntax
-       val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
-   in goalw_cterm defs g
-   end;
+  case termination_goals rules of
+      [] => error "tgoalw: no termination conditions to prove"
+    | L  => goalw_cterm defs 
+              (cterm_of (sign_of thy) 
+	                (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
 
 fun tgoal thy = tgoalw thy [];
isabelle