--- a/src/HOL/Tools/recfun_codegen.ML Wed Jan 13 10:18:45 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Wed Jan 13 12:20:37 2010 +0100
@@ -36,7 +36,7 @@
let val (_, T) = Code.const_typ_eqn thy thm
in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
then [thm]
- else [Code_Thingol.expand_eta thy 1 thm]
+ else [Code.expand_eta thy 1 thm]
end
| avoid_value thy thms = thms;
@@ -44,8 +44,9 @@
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
- |> Code.eqns_of_cert thy
- |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+ |> Code.equations_thms_cert thy
+ |> snd
+ |> map_filter (fn (_, (thm, proper)) => if proper 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
@@ -57,7 +58,6 @@
raw_thms
|> preprocess thy
|> avoid_value thy
- |> Code_Thingol.canonize_thms thy
|> rpair module_name
end;