# HG changeset patch
# User blanchet
# Date 1444204963 -7200
# Node ID d7215449be83ee8d53e8f693b288bd80e78196a7
# Parent  2ebdd603cd71040e454d511a8dfa63f08717d230
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier

diff -r 2ebdd603cd71 -r d7215449be83 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/String.thy	Wed Oct 07 10:02:43 2015 +0200
@@ -8,7 +8,7 @@
 
 subsection \<open>Characters and strings\<close>
 
-datatype nibble =
+datatype (plugins del: transfer) nibble =
     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
 
diff -r 2ebdd603cd71 -r d7215449be83 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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);
diff -r 2ebdd603cd71 -r d7215449be83 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Wed Oct 07 10:02:43 2015 +0200
@@ -154,7 +154,7 @@
        |> Thm.close_derivation
      end);
 
-val _ = Theory.setup (lfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin
   lfp_rec_sugar_transfer_interpretation);
 
 end;
diff -r 2ebdd603cd71 -r d7215449be83 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Oct 07 10:02:43 2015 +0200
@@ -1604,7 +1604,7 @@
       --| @{keyword ")"}) []) --
     (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
 
-val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
   gfp_rec_sugar_transfer_interpretation);
 
 end;
diff -r 2ebdd603cd71 -r d7215449be83 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Oct 06 21:04:44 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Oct 07 10:02:43 2015 +0200
@@ -8,7 +8,6 @@
 sig
   exception NO_PRED_DATA of unit
 
-  val transfer_plugin: string
   val base_name_of_bnf: BNF_Def.bnf -> binding
   val type_name_of_bnf: BNF_Def.bnf -> string
   val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
@@ -25,8 +24,6 @@
 
 exception NO_PRED_DATA of unit
 
-val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
-
 (* util functions *)
 
 fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))