# HG changeset patch
# User paulson
# Date 868012351 -7200
# Node ID 122e80826c95a3f6181101dea66d63b1885307a2
# Parent  32e7edc609fd86d56d9f9317966113d8d8b3170d
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

diff -r 32e7edc609fd -r 122e80826c95 TFL/post.sml
--- 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 [];