TFL/post.sml
changeset 3497 122e80826c95
parent 3459 112cbb8301dc
child 3556 229a40c2b19e
--- 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 [];