# HG changeset patch
# User haftmann
# Date 1266573981 -3600
# Node ID dfbcff38c9ed1dff8c0e3eab19be5eca39c4f7f5
# Parent  1c9866c5f6fbd39c6df823d5b16b959e6d78597b
using Code.bare_thms_of_cert

diff -r 1c9866c5f6fb -r dfbcff38c9ed src/HOL/Tools/recfun_codegen.ML
--- 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