src/HOL/Tools/BNF/bnf_lfp.ML
changeset 64413 c0d5e78eb647
parent 63826 9321b3d50abd
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 26 20:59:36 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 26 22:40:28 2016 +0200
     1.3 @@ -1303,7 +1303,7 @@
     1.4          ctor_Irel_thms, Ibnf_notes, lthy) =
     1.5        if m = 0 then
     1.6          (timer, replicate n DEADID_bnf,
     1.7 -        map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
     1.8 +        map_split (`(mk_pointfree2 lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
     1.9          mk_ctor_map_unique_DEADID_thm (),
    1.10          replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
    1.11        else let
    1.12 @@ -1791,7 +1791,7 @@
    1.13        ||>> mk_Frees "IR" activeIphiTs;
    1.14  
    1.15      val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
    1.16 -      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    1.17 +      ctor_Imap_o_thms (map (mk_pointfree2 lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    1.18  
    1.19      val Irels = if m = 0 then map HOLogic.eq_const Ts
    1.20        else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;