src/HOL/Tools/recfun_codegen.ML
changeset 31036 64ff53fc0c0c
parent 30190 479806475f3c
child 31087 a95816259c77
equal deleted inserted replaced
31035:de0a20a030fd 31036:64ff53fc0c0c
    57     val thms = Code.these_raw_eqns thy c'
    57     val thms = Code.these_raw_eqns thy c'
    58       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    58       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    59       |> expand_eta thy
    59       |> expand_eta thy
    60       |> map (AxClass.overload thy)
    60       |> map (AxClass.overload thy)
    61       |> map_filter (meta_eq_to_obj_eq thy)
    61       |> map_filter (meta_eq_to_obj_eq thy)
    62       |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
    62       |> Code_Unit.norm_varnames thy
    63       |> map (rpair opt_name)
    63       |> map (rpair opt_name)
    64   in if null thms then NONE else SOME thms end;
    64   in if null thms then NONE else SOME thms end;
    65 
    65 
    66 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    66 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    67 val const_of = dest_Const o head_of o fst o dest_eqn;
    67 val const_of = dest_Const o head_of o fst o dest_eqn;