--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 07 10:02:43 2015 +0200
@@ -64,6 +64,8 @@
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar}
+ val transfer_plugin: string
+
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
@@ -254,6 +256,8 @@
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar};
+val transfer_plugin = Plugin_Name.declare_setup @{binding transfer};
+
fun co_induct_of (i :: _) = i;
fun strong_co_induct_of [_, s] = s;
@@ -636,24 +640,27 @@
end;
in
if live = 0 then
- let
- val relAsBs = HOLogic.eq_const fpT;
- val rel_cases_thm = derive_rel_cases relAsBs [] [];
-
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
-
- val notes =
- [(case_transferN, [case_transfer_thm], K [])]
- |> massage_simple_notes fp_b_name;
-
- val (noted, lthy') = lthy
- |> Local_Theory.notes notes;
-
- val subst = Morphism.thm (substitute_noted_thm noted);
- in
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
- lthy')
- end
+ if plugins transfer_plugin then
+ let
+ val relAsBs = HOLogic.eq_const fpT;
+ val rel_cases_thm = derive_rel_cases relAsBs [] [];
+
+ val case_transfer_thm = derive_case_transfer rel_cases_thm;
+
+ val notes =
+ [(case_transferN, [case_transfer_thm], K [])]
+ |> massage_simple_notes fp_b_name;
+
+ val (noted, lthy') = lthy
+ |> Local_Theory.notes notes;
+
+ val subst = Morphism.thm (substitute_noted_thm noted);
+ in
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
+ lthy')
+ end
+ else
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
else
let
val mapx = mk_map live As Bs (map_of_bnf fp_bnf);