Now catches the error of calling tgoalw when there are no goals to prove,
authorpaulson
Fri Jul 04 12:32:31 1997 +0200 (1997-07-04)
changeset 3497122e80826c95
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
     1.1 --- a/TFL/post.sml	Fri Jul 04 12:31:20 1997 +0200
     1.2 +++ b/TFL/post.sml	Fri Jul 04 12:32:31 1997 +0200
     1.3 @@ -53,11 +53,11 @@
     1.4   * puts them into a goalstack.
     1.5   *--------------------------------------------------------------------------*)
     1.6  fun tgoalw thy defs rules = 
     1.7 -   let val L = termination_goals rules
     1.8 -       open USyntax
     1.9 -       val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
    1.10 -   in goalw_cterm defs g
    1.11 -   end;
    1.12 +  case termination_goals rules of
    1.13 +      [] => error "tgoalw: no termination conditions to prove"
    1.14 +    | L  => goalw_cterm defs 
    1.15 +              (cterm_of (sign_of thy) 
    1.16 +	                (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
    1.17  
    1.18  fun tgoal thy = tgoalw thy [];
    1.19