diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Wed Oct 18 10:15:39 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Wed Oct 18 16:13:03 2006 +0200
@@ -17,6 +17,7 @@
 struct
 
 
+open FundefLib
 open FundefCommon
 open FundefAbbrev
 
@@ -25,7 +26,7 @@
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
     in
-      Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
+      Trueprop (mk_acc domT R $ x)
     end
 
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =