making 'pred_inject' a first-class BNF citizen
authorblanchet
Wed Feb 17 17:08:36 2016 +0100 (2016-02-17)
changeset 62335e85c42f4f30a
parent 62334 15176172701e
child 62336 4a8d2f0d7fdd
making 'pred_inject' a first-class BNF citizen
NEWS
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/Basic_BNF_LFPs.thy
src/HOL/Basic_BNFs.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
     1.1 --- a/NEWS	Wed Feb 17 17:08:03 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 17:08:36 2016 +0100
     1.3 @@ -27,6 +27,10 @@
     1.4      "bnf" outputs a new proof obligation expressing pred in terms of set
     1.5         (not giving a specification for pred makes this one reflexive)
     1.6      INCOMPATIBILITY: manual "bnf" declarations may need adjustment
     1.7 +  - Renamed lemmas:
     1.8 +      rel_prod_apply ~> rel_prod_inject
     1.9 +      pred_prod_apply ~> pred_prod_inject
    1.10 +    INCOMPATIBILITY.
    1.11  
    1.12  
    1.13  New in Isabelle2016 (February 2016)
     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Wed Feb 17 17:08:03 2016 +0100
     2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Wed Feb 17 17:08:36 2016 +0100
     2.3 @@ -236,6 +236,12 @@
     2.4  lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
     2.5    unfolding rel_fun_def by simp
     2.6  
     2.7 +lemma eq_onp_live_step: "x = y \<Longrightarrow> eq_onp P a a \<and> x \<longleftrightarrow> P a \<and> y"
     2.8 +  by (simp only: eq_onp_same_args)
     2.9 +
    2.10 +lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
    2.11 +  by blast+
    2.12 +
    2.13  ML_file "Tools/BNF/bnf_fp_util.ML"
    2.14  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    2.15  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
     3.1 --- a/src/HOL/Basic_BNF_LFPs.thy	Wed Feb 17 17:08:03 2016 +0100
     3.2 +++ b/src/HOL/Basic_BNF_LFPs.thy	Wed Feb 17 17:08:36 2016 +0100
     3.3 @@ -97,7 +97,7 @@
     3.4  
     3.5  ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     3.6  
     3.7 -lemma size_bool[code]: "size (b::bool) = 0"
     3.8 +lemma size_bool[code]: "size (b :: bool) = 0"
     3.9    by (cases b) auto
    3.10  
    3.11  declare prod.size[no_atp]
     4.1 --- a/src/HOL/Basic_BNFs.thy	Wed Feb 17 17:08:03 2016 +0100
     4.2 +++ b/src/HOL/Basic_BNFs.thy	Wed Feb 17 17:08:36 2016 +0100
     4.3 @@ -36,6 +36,11 @@
     4.4    "P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)"
     4.5  | "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)"
     4.6  
     4.7 +lemma pred_sum_inject[code, simp]:
     4.8 +  "pred_sum P1 P2 (Inl a) \<longleftrightarrow> P1 a"
     4.9 +  "pred_sum P1 P2 (Inr b) \<longleftrightarrow> P2 b"
    4.10 +  by (simp add: pred_sum.simps)+
    4.11 +
    4.12  bnf "'a + 'b"
    4.13    map: map_sum
    4.14    sets: setl setr
    4.15 @@ -114,11 +119,11 @@
    4.16  where
    4.17    "\<lbrakk>P1 a; P2 b\<rbrakk> \<Longrightarrow> pred_prod P1 P2 (a, b)"
    4.18  
    4.19 -lemma rel_prod_apply [code, simp]:
    4.20 +lemma rel_prod_inject [code, simp]:
    4.21    "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    4.22    by (auto intro: rel_prod.intros elim: rel_prod.cases)
    4.23  
    4.24 -lemma pred_prod_apply [code, simp]:
    4.25 +lemma pred_prod_inject [code, simp]:
    4.26    "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    4.27    by (auto intro: pred_prod.intros elim: pred_prod.cases)
    4.28  
    4.29 @@ -178,7 +183,7 @@
    4.30    show "rel_prod R S = (\<lambda>x y.
    4.31      \<exists>z. ({fst z} \<subseteq> {(x, y). R x y} \<and> {snd z} \<subseteq> {(x, y). S x y}) \<and>
    4.32        map_prod fst fst z = x \<and> map_prod snd snd z = y)"
    4.33 -  unfolding prod_set_defs rel_prod_apply relcompp.simps conversep.simps fun_eq_iff
    4.34 +  unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff
    4.35    by auto
    4.36  qed auto
    4.37  
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 17 17:08:03 2016 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 17 17:08:36 2016 +0100
     5.3 @@ -27,6 +27,7 @@
     5.4       rel_sels: thm list,
     5.5       rel_intros: thm list,
     5.6       rel_cases: thm list,
     5.7 +     pred_injects: thm list,
     5.8       set_thms: thm list,
     5.9       set_selssss: thm list list list list,
    5.10       set_introssss: thm list list list list,
    5.11 @@ -195,6 +196,7 @@
    5.12  val map_disc_iffN = "map_disc_iff";
    5.13  val map_o_corecN = "map_o_corec";
    5.14  val map_selN = "map_sel";
    5.15 +val pred_injectN = "pred_inject";
    5.16  val rec_o_mapN = "rec_o_map";
    5.17  val rec_transferN = "rec_transfer";
    5.18  val set_casesN = "set_cases";
    5.19 @@ -221,6 +223,7 @@
    5.20     rel_sels: thm list,
    5.21     rel_intros: thm list,
    5.22     rel_cases: thm list,
    5.23 +   pred_injects: thm list,
    5.24     set_thms: thm list,
    5.25     set_selssss: thm list list list list,
    5.26     set_introssss: thm list list list list,
    5.27 @@ -265,7 +268,7 @@
    5.28  fun strong_co_induct_of [_, s] = s;
    5.29  
    5.30  fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts,
    5.31 -    rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss,
    5.32 +    rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
    5.33      set_cases} : fp_bnf_sugar) =
    5.34    {map_thms = map (Morphism.thm phi) map_thms,
    5.35     map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
    5.36 @@ -275,6 +278,7 @@
    5.37     rel_sels = map (Morphism.thm phi) rel_sels,
    5.38     rel_intros = map (Morphism.thm phi) rel_intros,
    5.39     rel_cases = map (Morphism.thm phi) rel_cases,
    5.40 +   pred_injects = map (Morphism.thm phi) pred_injects,
    5.41     set_thms = map (Morphism.thm phi) set_thms,
    5.42     set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss,
    5.43     set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss,
    5.44 @@ -369,10 +373,10 @@
    5.45  fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
    5.46      live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars co_recs co_rec_defs
    5.47      map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
    5.48 -    rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
    5.49 -    set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
    5.50 -    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
    5.51 -    set_inductss sel_transferss co_rec_o_mapss noted =
    5.52 +    rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss
    5.53 +    set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss
    5.54 +    co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss
    5.55 +    common_set_inducts set_inductss sel_transferss co_rec_o_mapss noted =
    5.56    let
    5.57      val fp_sugars =
    5.58        map_index (fn (kk, T) =>
    5.59 @@ -398,6 +402,7 @@
    5.60              rel_sels = nth rel_selss kk,
    5.61              rel_intros = nth rel_intross kk,
    5.62              rel_cases = nth rel_casess kk,
    5.63 +            pred_injects = nth pred_injectss kk,
    5.64              set_thms = nth set_thmss kk,
    5.65              set_selssss = nth set_selsssss kk,
    5.66              set_introssss = nth set_introsssss kk,
    5.67 @@ -566,10 +571,10 @@
    5.68        b_names Ts thmss)
    5.69    #> filter_out (null o fst o hd o snd);
    5.70  
    5.71 -fun derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps
    5.72 -    live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs fp_b_name fp_bnf fpT ctor
    5.73 -    ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm
    5.74 -    ctr_Tss abs
    5.75 +fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
    5.76 +    fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
    5.77 +    live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
    5.78 +    dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
    5.79      ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
    5.80        injects, distincts, distinct_discsss, ...} : ctr_sugar)
    5.81      lthy =
    5.82 @@ -582,13 +587,15 @@
    5.83  
    5.84      val fpBT = B_ify_T fpT;
    5.85      val live_AsBs = filter (op <>) (As ~~ Bs);
    5.86 +    val live_As = map fst live_AsBs;
    5.87      val fTs = map (op -->) live_AsBs;
    5.88  
    5.89 -    val (((((((xss, yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy
    5.90 +    val ((((((((xss, yss), fs), Ps), Rs), ta), tb), thesis), names_lthy) = lthy
    5.91        |> fold (fold Variable.declare_typ) [As, Bs]
    5.92        |> mk_Freess "x" ctr_Tss
    5.93        ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
    5.94        ||>> mk_Frees "f" fTs
    5.95 +      ||>> mk_Frees "P" (map mk_pred1T live_As)
    5.96        ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
    5.97        ||>> yield_singleton (mk_Frees "a") fpT
    5.98        ||>> yield_singleton (mk_Frees "b") fpBT
    5.99 @@ -597,7 +604,7 @@
   5.100      val ctrAs = map (mk_ctr As) ctrs;
   5.101      val ctrBs = map (mk_ctr Bs) ctrs;
   5.102  
   5.103 -    fun derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms =
   5.104 +    fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms =
   5.105        let
   5.106          val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
   5.107  
   5.108 @@ -622,13 +629,13 @@
   5.109          val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
   5.110        in
   5.111          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   5.112 -          mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
   5.113 +          mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
   5.114              rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
   5.115          |> singleton (Proof_Context.export names_lthy lthy)
   5.116          |> Thm.close_derivation
   5.117        end;
   5.118  
   5.119 -    fun derive_case_transfer rel_cases_thm =
   5.120 +    fun derive_case_transfer rel_case_thm =
   5.121        let
   5.122          val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
   5.123          val caseA = mk_case As C casex;
   5.124 @@ -636,7 +643,7 @@
   5.125          val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB;
   5.126        in
   5.127          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   5.128 -          mk_case_transfer_tac ctxt rel_cases_thm case_thms)
   5.129 +          mk_case_transfer_tac ctxt rel_case_thm case_thms)
   5.130          |> singleton (Proof_Context.export names_lthy lthy)
   5.131          |> Thm.close_derivation
   5.132        end;
   5.133 @@ -645,9 +652,9 @@
   5.134        if plugins transfer_plugin then
   5.135          let
   5.136            val relAsBs = HOLogic.eq_const fpT;
   5.137 -          val rel_cases_thm = derive_rel_cases relAsBs [] [];
   5.138 -
   5.139 -          val case_transfer_thm = derive_case_transfer rel_cases_thm;
   5.140 +          val rel_case_thm = derive_rel_case relAsBs [] [];
   5.141 +
   5.142 +          val case_transfer_thm = derive_case_transfer rel_case_thm;
   5.143  
   5.144            val notes =
   5.145              [(case_transferN, [case_transfer_thm], K [])]
   5.146 @@ -658,11 +665,11 @@
   5.147  
   5.148            val subst = Morphism.thm (substitute_noted_thm noted);
   5.149          in
   5.150 -          (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
   5.151 -           lthy')
   5.152 +          (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [],
   5.153 +            []), lthy')
   5.154          end
   5.155        else
   5.156 -        (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
   5.157 +        (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
   5.158      else
   5.159        let
   5.160          val mapx = mk_map live As Bs (map_of_bnf fp_bnf);
   5.161 @@ -891,7 +898,8 @@
   5.162                         (map (rapp ta) selAs) (map (rapp tb) selBs)))]);
   5.163  
   5.164              val goals =
   5.165 -              if n = 0 then []
   5.166 +              if n = 0 then
   5.167 +                []
   5.168                else
   5.169                  [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
   5.170                     (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
   5.171 @@ -909,9 +917,9 @@
   5.172              map prove goals
   5.173            end;
   5.174  
   5.175 -        val (rel_cases_thm, rel_cases_attrs) =
   5.176 +        val (rel_case_thm, rel_case_attrs) =
   5.177            let
   5.178 -            val thm = derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms;
   5.179 +            val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms;
   5.180              val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs);
   5.181              val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
   5.182              val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   5.183 @@ -920,16 +928,18 @@
   5.184              (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
   5.185            end;
   5.186  
   5.187 -        val case_transfer_thm = derive_case_transfer rel_cases_thm;
   5.188 +        val case_transfer_thm = derive_case_transfer rel_case_thm;
   5.189  
   5.190          val sel_transfer_thms =
   5.191 -          if null selAss then []
   5.192 +          if null selAss then
   5.193 +            []
   5.194            else
   5.195              let
   5.196                val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss));
   5.197                val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels;
   5.198              in
   5.199 -              if null goals then []
   5.200 +              if null goals then
   5.201 +                []
   5.202                else
   5.203                  let
   5.204                    val goal = Logic.mk_conjunction_balanced goals;
   5.205 @@ -1092,6 +1102,51 @@
   5.206                  end)
   5.207            end;
   5.208  
   5.209 +        val pred_injects =
   5.210 +          let
   5.211 +            fun top_sweep_rewr_conv rewrs =
   5.212 +              Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context};
   5.213 +
   5.214 +            val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
   5.215 +              (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})));
   5.216 +
   5.217 +            val eq_onps = map (rel_eq_onp_with_tops_of)
   5.218 +              (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps);
   5.219 +            val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As);
   5.220 +            val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps);
   5.221 +
   5.222 +            val get_rhs = Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> snd;
   5.223 +
   5.224 +            val pred_eq_onp_conj =
   5.225 +              List.foldr (fn (_, thm) => thm RS @{thm eq_onp_live_step}) @{thm refl[of True]};
   5.226 +
   5.227 +            fun predify_rel_inject rel_inject =
   5.228 +              let
   5.229 +                val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default [];
   5.230 +
   5.231 +                fun postproc thm =
   5.232 +                  if conjuncts <> [] then
   5.233 +                    @{thm box_equals} OF [thm, @{thm eq_onp_same_args},
   5.234 +                      pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}]
   5.235 +                  else
   5.236 +                    thm RS (@{thm eq_onp_same_args} RS iffD1);
   5.237 +              in
   5.238 +                rel_inject
   5.239 +                |> Thm.instantiate' cTs cts
   5.240 +                |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
   5.241 +                  (Raw_Simplifier.rewrite lthy false
   5.242 +                     @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
   5.243 +                |> unfold_thms lthy eq_onps
   5.244 +                |> postproc
   5.245 +                |> unfold_thms lthy @{thms top_conj}
   5.246 +              end;
   5.247 +          in
   5.248 +            rel_inject_thms
   5.249 +            |> map (unfold_thms lthy [@{thm conj_assoc}])
   5.250 +            |> map predify_rel_inject
   5.251 +            |> Proof_Context.export names_lthy lthy
   5.252 +          end;
   5.253 +
   5.254          val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
   5.255  
   5.256          val anonymous_notes =
   5.257 @@ -1106,7 +1161,8 @@
   5.258             (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
   5.259             (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
   5.260             (map_selN, map_sel_thms, K []),
   5.261 -           (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
   5.262 +           (pred_injectN, pred_injects, K simp_attrs),
   5.263 +           (rel_casesN, [rel_case_thm], K rel_case_attrs),
   5.264             (rel_distinctN, rel_distinct_thms, K simp_attrs),
   5.265             (rel_injectN, rel_inject_thms, K simp_attrs),
   5.266             (rel_introsN, rel_intro_thms, K []),
   5.267 @@ -1133,7 +1189,8 @@
   5.268            map subst rel_distinct_thms,
   5.269            map subst rel_sel_thms,
   5.270            map subst rel_intro_thms,
   5.271 -          [subst rel_cases_thm],
   5.272 +          [subst rel_case_thm],
   5.273 +          map subst pred_injects,
   5.274            map subst set_thms,
   5.275            map (map (map (map subst))) set_sel_thmssss,
   5.276            map (map (map (map subst))) set_intros_thmssss,
   5.277 @@ -2143,10 +2200,12 @@
   5.278      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   5.279      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   5.280      val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
   5.281 +    val fp_nesting_rel_eq_onps = map rel_eq_onp_of_bnf fp_nesting_bnfs;
   5.282      val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs;
   5.283      val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
   5.284      val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
   5.285      val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
   5.286 +    val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs;
   5.287  
   5.288      val live = live_of_bnf any_fp_bnf;
   5.289      val _ =
   5.290 @@ -2287,10 +2346,11 @@
   5.291        in
   5.292          (wrap_ctrs
   5.293           #> (fn (ctr_sugar, lthy) =>
   5.294 -           derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs'
   5.295 -             fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
   5.296 -             fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def
   5.297 -             fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ctr_sugar lthy
   5.298 +           derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
   5.299 +             fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
   5.300 +             live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
   5.301 +             ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
   5.302 +             fp_rel_thm ctr_Tss abs ctr_sugar lthy
   5.303             |>> pair ctr_sugar)
   5.304           ##>>
   5.305             (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
   5.306 @@ -2298,9 +2358,9 @@
   5.307           #> massage_res, lthy')
   5.308        end;
   5.309  
   5.310 -    fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
   5.311 +    fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
   5.312        fold_map I wrap_one_etc lthy
   5.313 -      |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 16} o split_list)
   5.314 +      |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list)
   5.315          o split_list;
   5.316  
   5.317      fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
   5.318 @@ -2337,7 +2397,8 @@
   5.319        end;
   5.320  
   5.321      fun derive_rec_o_map_thmss lthy recs rec_defs =
   5.322 -      if live = 0 then replicate nn []
   5.323 +      if live = 0 then
   5.324 +        replicate nn []
   5.325        else
   5.326          let
   5.327            fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
   5.328 @@ -2404,7 +2465,7 @@
   5.329  
   5.330      fun derive_note_induct_recs_thms_for_types
   5.331          ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
   5.332 -            rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss,
   5.333 +            rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
   5.334              set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
   5.335             (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
   5.336            (recs, rec_defs)), lthy) =
   5.337 @@ -2468,10 +2529,10 @@
   5.338            fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
   5.339            recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
   5.340            (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
   5.341 -          rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
   5.342 -          case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
   5.343 -          common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
   5.344 -          rec_o_map_thmss
   5.345 +          rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
   5.346 +          ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn [])
   5.347 +          rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
   5.348 +          sel_transferss rec_o_map_thmss
   5.349        end;
   5.350  
   5.351      fun derive_corec_transfer_thms lthy corecs corec_defs =
   5.352 @@ -2491,7 +2552,8 @@
   5.353        end;
   5.354  
   5.355      fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
   5.356 -      if live = 0 then replicate nn []
   5.357 +      if live = 0 then
   5.358 +        replicate nn []
   5.359        else
   5.360          let
   5.361            fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
   5.362 @@ -2551,8 +2613,8 @@
   5.363  
   5.364      fun derive_note_coinduct_corecs_thms_for_types
   5.365          ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
   5.366 -            rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess,
   5.367 -            ctr_transferss, case_transferss, disc_transferss, sel_transferss),
   5.368 +            rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
   5.369 +            set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
   5.370             (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
   5.371            (corecs, corec_defs)), lthy) =
   5.372        let
   5.373 @@ -2647,10 +2709,11 @@
   5.374            corecs corec_defs map_thmss [coinduct_thm, coinduct_strong_thm]
   5.375            (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
   5.376            corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
   5.377 -          rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
   5.378 -          case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
   5.379 -          corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
   5.380 -          (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss map_o_corec_thmss
   5.381 +          rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
   5.382 +          ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss
   5.383 +          (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms
   5.384 +          rel_coinduct_thmss set_induct_thms (replicate nn (if nn = 1 then set_induct_thms else []))
   5.385 +          sel_transferss map_o_corec_thmss
   5.386        end;
   5.387  
   5.388      val lthy'' = lthy'
   5.389 @@ -2659,7 +2722,7 @@
   5.390          xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
   5.391          xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
   5.392          ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
   5.393 -      |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
   5.394 +      |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types
   5.395        |> case_fp fp derive_note_induct_recs_thms_for_types
   5.396             derive_note_coinduct_corecs_thms_for_types;
   5.397  
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Feb 17 17:08:03 2016 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Feb 17 17:08:36 2016 +0100
     6.3 @@ -40,8 +40,8 @@
     6.4      tactic
     6.5    val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
     6.6      term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
     6.7 -  val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
     6.8 -    thm list -> thm list -> thm list -> tactic
     6.9 +  val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
    6.10 +    thm list -> thm list -> tactic
    6.11    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
    6.12      thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    6.13      thm list -> thm list -> thm list -> tactic
    6.14 @@ -79,7 +79,7 @@
    6.15    @{thms UN_empty UN_insert  UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
    6.16         o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
    6.17  val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
    6.18 -val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
    6.19 +val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc};
    6.20  
    6.21  fun is_def_looping def =
    6.22    (case Thm.prop_of def of
    6.23 @@ -103,10 +103,10 @@
    6.24  
    6.25  val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
    6.26  
    6.27 -fun mk_case_transfer_tac ctxt rel_cases cases =
    6.28 -  let val n = length (tl (Thm.prems_of rel_cases)) in
    6.29 +fun mk_case_transfer_tac ctxt rel_case cases =
    6.30 +  let val n = length (tl (Thm.prems_of rel_case)) in
    6.31      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
    6.32 -    HEADGOAL (etac ctxt rel_cases) THEN
    6.33 +    HEADGOAL (etac ctxt rel_case) THEN
    6.34      ALLGOALS (hyp_subst_tac ctxt) THEN
    6.35      unfold_thms_tac ctxt cases THEN
    6.36      ALLGOALS (fn k => (select_prem_tac ctxt n (dtac ctxt asm_rl) k) k) THEN
    6.37 @@ -408,7 +408,7 @@
    6.38      unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
    6.39      ALLGOALS (rtac ctxt refl);
    6.40  
    6.41 -fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
    6.42 +fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
    6.43    HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
    6.44      rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
    6.45        hyp_subst_tac ctxt) THEN
    6.46 @@ -436,7 +436,7 @@
    6.47        unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
    6.48        unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
    6.49          abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
    6.50 -        @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
    6.51 +        @{thms id_bnf_def rel_sum_simps rel_prod_inject vimage2p_def Inl_Inr_False
    6.52            iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
    6.53        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN'
    6.54          (REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt))))
    6.55 @@ -454,7 +454,7 @@
    6.56          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    6.57            @{thms id_bnf_def vimage2p_def}) THEN
    6.58          TRYALL (hyp_subst_tac ctxt) THEN
    6.59 -        unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    6.60 +        unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_inject Inl_Inr_False
    6.61            Inr_Inl_False  sum.inject prod.inject}) THEN
    6.62          TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE'
    6.63            (REPEAT_DETERM o etac ctxt conjE) THEN' assume_tac ctxt))
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 17 17:08:03 2016 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 17 17:08:36 2016 +0100
     7.3 @@ -299,7 +299,8 @@
     7.4              co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
     7.5              ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
     7.6                fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
     7.7 -                rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
     7.8 +                rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
     7.9 +                set_cases, ...},
    7.10                fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
    7.11                  co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
    7.12                  set_inducts, ...},
    7.13 @@ -325,6 +326,7 @@
    7.14                rel_sels = rel_sels,
    7.15                rel_intros = rel_intros,
    7.16                rel_cases = rel_cases,
    7.17 +              pred_injects = pred_injects,
    7.18                set_thms = set_thms,
    7.19                set_selssss = set_selssss,
    7.20                set_introssss = set_introssss,
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 17 17:08:03 2016 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 17 17:08:36 2016 +0100
     8.3 @@ -661,7 +661,7 @@
     8.4  
     8.5      val timer = time (timer "FP construction in total");
     8.6    in
     8.7 -    timer; ((pre_bnfs, absT_infos), res)
     8.8 +    ((pre_bnfs, absT_infos), res)
     8.9    end;
    8.10  
    8.11  fun fp_antiquote_setup binding =
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Feb 17 17:08:03 2016 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Feb 17 17:08:36 2016 +0100
     9.3 @@ -90,6 +90,7 @@
     9.4          rel_sels = @{thms rel_sum_sel},
     9.5          rel_intros = @{thms rel_sum.intros},
     9.6          rel_cases = @{thms rel_sum.cases},
     9.7 +        pred_injects = @{thms pred_sum_inject},
     9.8          set_thms = @{thms sum_set_simps},
     9.9          set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
    9.10          set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
    9.11 @@ -154,11 +155,12 @@
    9.12         {map_thms = @{thms map_prod_simp},
    9.13          map_disc_iffs = [],
    9.14          map_selss = [@{thms fst_map_prod snd_map_prod}],
    9.15 -        rel_injects = @{thms rel_prod_apply},
    9.16 +        rel_injects = @{thms rel_prod_inject},
    9.17          rel_distincts = [],
    9.18          rel_sels = @{thms rel_prod_sel},
    9.19          rel_intros = @{thms rel_prod.intros},
    9.20          rel_cases = @{thms rel_prod.cases},
    9.21 +        pred_injects = @{thms pred_prod_inject},
    9.22          set_thms = @{thms prod_set_simps},
    9.23          set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
    9.24          set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],
    10.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Feb 17 17:08:03 2016 +0100
    10.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Feb 17 17:08:36 2016 +0100
    10.3 @@ -36,14 +36,6 @@
    10.4      Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
    10.5    end
    10.6  
    10.7 -fun mk_eq_onp arg =
    10.8 -  let
    10.9 -    val argT = domain_type (fastype_of arg)
   10.10 -  in
   10.11 -    Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
   10.12 -      $ arg
   10.13 -  end
   10.14 -
   10.15  fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
   10.16  
   10.17  fun is_Type (Type _) = true
   10.18 @@ -252,57 +244,6 @@
   10.19      SOME data => data
   10.20    | NONE => raise NO_PRED_DATA ()
   10.21  
   10.22 -val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
   10.23 -  (Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})));
   10.24 -
   10.25 -fun prove_pred_inject lthy ({T = fpT, fp_nesting_bnfs, live_nesting_bnfs,
   10.26 -    fp_res = {bnfs = fp_bnfs, ...}, fp_bnf_sugar = {rel_injects, ...}, ...} : fp_sugar) =
   10.27 -  let
   10.28 -    val As = snd (dest_Type fpT)
   10.29 -    val liveness = liveness_of_fp_bnf (length As) (hd fp_bnfs)
   10.30 -    val lives = map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As)
   10.31 -
   10.32 -    val involved_bnfs = distinct (op = o @{apply 2} BNF_Def.T_of_bnf)
   10.33 -      (fp_nesting_bnfs @ live_nesting_bnfs @ fp_bnfs)
   10.34 -    val eq_onps = map (rel_eq_onp_with_tops_of o rel_eq_onp_of_bnf) involved_bnfs
   10.35 -    val old_lthy = lthy
   10.36 -    val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp lives) lthy
   10.37 -    val predTs = map mk_pred1T As
   10.38 -    val (preds, lthy) = mk_Frees "P" predTs lthy
   10.39 -    val args = map mk_eq_onp preds
   10.40 -    val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) As)
   10.41 -    val cts = map (SOME o Thm.cterm_of lthy) args
   10.42 -    fun get_rhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
   10.43 -    fun is_eqn thm = can get_rhs thm
   10.44 -    fun rel2pred_massage thm =
   10.45 -      let
   10.46 -        val live_step = @{lemma "x = y \<Longrightarrow> (eq_onp P a a \<and> x) = (P a \<and> y)" by (simp only: eq_onp_same_args)}
   10.47 -        val kill_top1 = @{lemma "(top x \<and> P) = P" by blast}
   10.48 -        val kill_top2 = @{lemma "(P \<and> top x) = P" by blast}
   10.49 -        fun pred_eq_onp_conj conjs = List.foldr (fn (_, thm) => thm RS live_step)
   10.50 -          @{thm refl[of True]} conjs
   10.51 -        val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else []
   10.52 -        val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1]
   10.53 -        val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
   10.54 -      in
   10.55 -        thm
   10.56 -        |> Thm.instantiate' cTs cts
   10.57 -        |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
   10.58 -          (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
   10.59 -        |> Local_Defs.unfold lthy eq_onps
   10.60 -        |> (fn thm => if conjuncts <> [] then @{thm box_equals}
   10.61 -              OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True]
   10.62 -            else thm RS (@{thm eq_onp_same_args} RS iffD1))
   10.63 -        |> kill_top
   10.64 -      end
   10.65 -  in
   10.66 -    rel_injects
   10.67 -    |> map (Local_Defs.unfold lthy [@{thm conj_assoc}])
   10.68 -    |> map rel2pred_massage
   10.69 -    |> Variable.export lthy old_lthy
   10.70 -    |> map Drule.zero_var_indexes
   10.71 -  end
   10.72 -
   10.73  
   10.74  (* fp_sugar interpretation *)
   10.75  
   10.76 @@ -317,28 +258,22 @@
   10.77      map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules
   10.78    end
   10.79  
   10.80 -fun pred_injects fp_sugar lthy =
   10.81 +fun register_pred_injects fp_sugar lthy =
   10.82    let
   10.83 -    val pred_injects = prove_pred_inject lthy fp_sugar
   10.84 -    fun qualify defname suffix = Binding.qualified true suffix defname
   10.85 -    val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
   10.86 -    val simp_attrs = @{attributes [simp]}
   10.87 +    val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar)
   10.88      val type_name = type_name_of_bnf (#fp_bnf fp_sugar)
   10.89      val pred_data = lookup_defined_pred_data lthy type_name 
   10.90        |> Transfer.update_pred_simps pred_injects
   10.91    in
   10.92      lthy 
   10.93 -    |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) 
   10.94 -    |> snd
   10.95      |> Local_Theory.declaration {syntax = false, pervasive = true}
   10.96        (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
   10.97      |> Local_Theory.restore
   10.98    end
   10.99  
  10.100 -
  10.101  fun transfer_fp_sugars_interpretation fp_sugar lthy =
  10.102    let
  10.103 -    val lthy = pred_injects fp_sugar lthy
  10.104 +    val lthy = register_pred_injects fp_sugar lthy
  10.105      val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
  10.106    in
  10.107      lthy