# HG changeset patch
# User blanchet
# Date 1473155739 -7200
# Node ID 83841a5c08973401ea25be9882932d5e433a6af6
# Parent  6489d85ecc984212191628404f990992d3ed2968
extended ML signature + refactored

diff -r 6489d85ecc98 -r 83841a5c0897 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 06 11:21:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 06 11:55:39 2016 +0200
@@ -7,6 +7,8 @@
 
 signature BNF_FP_REC_SUGAR_TRANSFER =
 sig
+  val set_transfer_rule_attrs: thm list -> local_theory -> local_theory
+
   val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
     Proof.context
   val gfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
@@ -27,6 +29,11 @@
 
 val transferN = "transfer";
 
+val transfer_rule_attrs = @{attributes [transfer_rule]};
+
+fun set_transfer_rule_attrs thms =
+  snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
+
 fun mk_lfp_rec_sugar_transfer_tac ctxt def =
   unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt);
 
@@ -150,11 +157,11 @@
      in
        Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
          mk_gfp_rec_sugar_transfer_tac ctxt def
-         (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk)))
-         (map (#type_definition o #absT_info) fp_sugars)
-         (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
-         (map (rel_def_of_bnf o #pre_bnf) fp_sugars)
-         disc_eq_cases case_thms case_distribs case_congs)
+           (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk)))
+           (map (#type_definition o #absT_info) fp_sugars)
+           (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
+           (map (rel_def_of_bnf o #pre_bnf) fp_sugars)
+           disc_eq_cases case_thms case_distribs case_congs)
        |> Thm.close_derivation
      end);
 
diff -r 6489d85ecc98 -r 83841a5c0897 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 06 11:21:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 06 11:55:39 2016 +0200
@@ -42,8 +42,9 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
+open BNF_GFP_Util
 open BNF_GFP_Rec_Sugar
-open BNF_GFP_Util
+open BNF_FP_Rec_Sugar_Transfer
 open BNF_GFP_Grec
 open BNF_GFP_Grec_Sugar_Util
 open BNF_GFP_Grec_Sugar_Tactics
@@ -75,7 +76,6 @@
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val transfer_rule_attrs = @{attributes [transfer_rule]};
 
 val unfold_id_thms1 =
   map (fn thm => thm RS eq_reflection) @{thms id_bnf_o o_id_bnf id_apply o_apply} @
@@ -284,9 +284,6 @@
   [mk_abs_transfer ctxt fpT_name, mk_rep_transfer ctxt fpT_name]
   handle Fail _ => [];
 
-fun set_transfer_rule_attrs thms =
-  snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
-
 fun ensure_codatatype_extra fpT_name ctxt =
   (case codatatype_extra_of ctxt fpT_name of
     NONE =>