Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
value restriction
authorhaftmann
Tue, 14 Nov 2006 09:06:08 +0100
changeset 21357 8ebff00544e5
parent 21356 556addc67737
child 21358 f48800c3d573
value restriction
src/HOL/Tools/function_package/fundef_common.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle