Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/recfun_codegen.ML
changeset 31962 baa8dce5bc45
parent 31958 2133f596c520
child 31998 2c7a24f74db9 
--- a/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 06:43:30 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 08:18:07 2009 +0200
@@ -26,7 +26,7 @@
 fun add_thm NONE thm thy = Code.add_eqn thm thy
   | add_thm (SOME module_name) thm thy =
       let
-        val (thm', _) = Code.mk_eqn thy (K false) (thm, true)
+        val (thm', _) = Code.mk_eqn thy (thm, true)
       in
         thy
         |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
isabelle