--- a/src/HOL/Tools/recfun_codegen.ML Mon May 11 09:40:39 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon May 11 10:53:19 2009 +0200
@@ -25,13 +25,13 @@
fun add_thm NONE thm thy = Code.add_eqn thm thy
| add_thm (SOME module_name) thm thy =
- case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
- of SOME (thm', _) => let val c = Code_Unit.const_eqn thy thm'
- in thy
- |> ModuleData.map (Symtab.update (c, module_name))
- |> Code.add_eqn thm'
- end
- | NONE => Code.add_eqn thm thy;
+ let
+ val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true)
+ in
+ thy
+ |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name))
+ |> Code.add_eqn thm'
+ end;
fun meta_eq_to_obj_eq thy thm =
let