--- a/src/HOL/Tools/recfun_codegen.ML Tue Jan 12 09:59:45 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Jan 12 16:27:42 2010 +0100
@@ -43,8 +43,10 @@
fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
let
val c = AxClass.unoverload_const thy (raw_c, T);
- val raw_thms = Code.these_eqns thy c
+ val raw_thms = Code.get_cert thy I c
+ |> Code.eqns_of_cert thy
|> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+ |> 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
of SOME module_name => module_name