src/HOL/Tools/function_package/termination.ML

--- a/src/HOL/Tools/function_package/termination.ML	Thu Oct 26 15:12:03 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Thu Oct 26 15:16:31 2006 +0200
@@ -26,7 +26,7 @@
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
     in
-      Trueprop (mk_acc domT R $ x)
+      mk_forall x (Trueprop (mk_acc domT R $ x))
     end
 
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =