src/HOL/Tools/recfun_codegen.ML
changeset 34895 19fd499cddff
parent 34893 ecdc526af73a
child 35225 dfbcff38c9ed
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 10:18:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jan 13 12:20:37 2010 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4        let val (_, T) = Code.const_typ_eqn thy thm
     1.5        in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
     1.6          then [thm]
     1.7 -        else [Code_Thingol.expand_eta thy 1 thm]
     1.8 +        else [Code.expand_eta thy 1 thm]
     1.9        end
    1.10    | avoid_value thy thms = thms;
    1.11  
    1.12 @@ -44,8 +44,9 @@
    1.13    let
    1.14      val c = AxClass.unoverload_const thy (raw_c, T);
    1.15      val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
    1.16 -      |> Code.eqns_of_cert thy
    1.17 -      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.18 +      |> Code.equations_thms_cert thy
    1.19 +      |> snd
    1.20 +      |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
    1.21        |> map (AxClass.overload thy)
    1.22        |> filter (is_instance T o snd o const_of o prop_of);
    1.23      val module_name = case Symtab.lookup (ModuleData.get thy) c
    1.24 @@ -57,7 +58,6 @@
    1.25      raw_thms
    1.26      |> preprocess thy
    1.27      |> avoid_value thy
    1.28 -    |> Code_Thingol.canonize_thms thy
    1.29      |> rpair module_name
    1.30    end;
    1.31