# HG changeset patch
# User haftmann
# Date 1163491568 -3600
# Node ID 8ebff00544e522598cf528725d03aad5af74c8f2
# Parent  556addc6773726bc888ed494692cfff0897c6801
value restriction

diff -r 556addc67737 -r 8ebff00544e5 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 14 00:18:57 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 14 09:06:08 2006 +0100
@@ -245,7 +245,7 @@
 (struct
     val name = "HOL/function_def/termination"
     type T = thm option
-    val init = K NONE
+    fun init _ = NONE
     fun print  _ _ = ()
 end);