TFL/post.ML
changeset 17959 8db36a108213
parent 17615 3c5b158be33c
child 18139 b15981aedb7b
--- a/TFL/post.ML	Fri Oct 21 18:14:37 2005 +0200
+++ b/TFL/post.ML	Fri Oct 21 18:14:38 2005 +0200
@@ -52,7 +52,7 @@
 fun tgoalw thy defs rules =
   case termination_goals rules of
       [] => error "tgoalw: no termination conditions to prove"
-    | L  => goalw_cterm defs
+    | L  => OldGoals.goalw_cterm defs
               (Thm.cterm_of (Theory.sign_of thy)
                         (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));