--- a/src/HOL/Tools/function_package/termination.ML Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML Wed Sep 13 12:05:50 2006 +0200
@@ -25,7 +25,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_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
end
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =