src/HOL/Tools/recfun_codegen.ML
changeset 31962 baa8dce5bc45
parent 31958 2133f596c520
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 06:43:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 08:18:07 2009 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  fun add_thm NONE thm thy = Code.add_eqn thm thy
     1.5    | add_thm (SOME module_name) thm thy =
     1.6        let
     1.7 -        val (thm', _) = Code.mk_eqn thy (K false) (thm, true)
     1.8 +        val (thm', _) = Code.mk_eqn thy (thm, true)
     1.9        in
    1.10          thy
    1.11          |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))