# 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 [];