--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -191,9 +191,7 @@
                            |> safe_mk_meta_eq)))
                        thy
 
-val case_cong = fold add_case_cong
-
-val setup_case_cong = DatatypePackage.interpretation case_cong
+val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
 
 
 (* setup *)