--- a/src/HOL/Tools/recfun_codegen.ML Fri Feb 19 11:06:20 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Feb 19 11:06:21 2010 +0100
@@ -44,9 +44,7 @@
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
- |> Code.equations_thms_cert thy
- |> snd
- |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
+ |> Code.bare_thms_of_cert thy
|> map (AxClass.overload thy)
|> filter (is_instance T o snd o const_of o prop_of);
val module_name = case Symtab.lookup (ModuleData.get thy) c