drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'

--- a/src/HOL/BNF_Examples/Compat.thy	Mon Sep 01 18:42:02 2014 +0200
+++ b/src/HOL/BNF_Examples/Compat.thy	Mon Sep 01 19:28:00 2014 +0200
@@ -58,7 +58,7 @@
 datatype_compat s
 
 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s}; \<close>
-ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name x}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
 
 datatype_compat x
 
@@ -66,7 +66,7 @@
 
 datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst"
 
-ML \<open> get_descrs @{theory} (0, 4, 1) @{type_name tttre}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close>
 
 datatype_compat tttre
 
@@ -74,7 +74,7 @@
 
 datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
 
-ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name ftre}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close>
 
 datatype_compat ftre
 
@@ -82,7 +82,7 @@
 
 datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst"
 
-ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name btre}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close>
 
 datatype_compat btre
 
@@ -100,7 +100,7 @@
 
 datatype_new 'a tre = Tre 'a "'a tre lst"
 
-ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name tre}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close>
 
 datatype_compat tre
 
@@ -124,7 +124,7 @@
 
 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f}; \<close>
 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g}; \<close>
-ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name h}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
 
 datatype_compat h
 
@@ -187,7 +187,7 @@
 
 datatype_new tree = Tree "tree foo"
 
-ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name tree}; \<close>
+ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close>
 
 datatype_compat tree
 

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 01 18:42:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 01 19:28:00 2014 +0200
@@ -11,12 +11,12 @@
   val unfold_splits_lets: term -> term
   val dest_map: Proof.context -> string -> term -> term * term list
 
-  val mutualize_fp_sugars: BNF_Util.fp_kind -> bool -> int list -> binding list -> typ list ->
-    term list -> term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
+  val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
+    term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
     (BNF_FP_Util.fp_sugar list
      * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
     * local_theory
-  val nested_to_mutual_fps: BNF_Util.fp_kind -> bool -> binding list -> typ list -> term list ->
+  val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
     (term * term list list) list list -> local_theory ->
     (typ list * int list * BNF_FP_Util.fp_sugar list
      * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
@@ -113,8 +113,8 @@
   |> map_filter I;
 
 (* TODO: test with sort constraints on As *)
-fun mutualize_fp_sugars fp need_co_inducts_recs cliques bs fpTs callers callssss
-    (fp_sugars0 as fp_sugars01 :: _) no_defs_lthy0 =
+fun mutualize_fp_sugars fp cliques bs fpTs callers callssss (fp_sugars0 as fp_sugars01 :: _)
+    no_defs_lthy0 =
   let
     val thy = Proof_Context.theory_of no_defs_lthy0;
 
@@ -228,73 +228,58 @@
 
         val fp_absT_infos = map #absT_info fp_sugars0;
 
-        val (fp_res, fp_nesting_bnfs, live_nesting_bnfs, common_co_inducts, pre_bnfs, absT_infos,
-             co_recs, co_rec_defs, co_inductss, co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss,
-             fp_sugar_thms, lthy) =
-          if need_co_inducts_recs then
-            let
-              val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
-                     dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-                fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
-                  no_defs_lthy0;
+          val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+                 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
+            fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
+              no_defs_lthy0;
 
-              val fp_abs_inverses = map #abs_inverse fp_absT_infos;
-              val fp_type_definitions = map #type_definition fp_absT_infos;
+          val fp_abs_inverses = map #abs_inverse fp_absT_infos;
+          val fp_type_definitions = map #type_definition fp_absT_infos;
 
-              val abss = map #abs absT_infos;
-              val reps = map #rep absT_infos;
-              val absTs = map #absT absT_infos;
-              val repTs = map #repT absT_infos;
-              val abs_inverses = map #abs_inverse absT_infos;
+          val abss = map #abs absT_infos;
+          val reps = map #rep absT_infos;
+          val absTs = map #absT absT_infos;
+          val repTs = map #repT absT_infos;
+          val abs_inverses = map #abs_inverse absT_infos;
 
-              val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
-              val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
+          val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+          val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
 
-              val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
-                mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+          val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
+            mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
 
-              fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
+          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
 
-              val ((co_recs, co_rec_defs), lthy) =
-                fold_map2 (fn b =>
-                    if fp = Least_FP then
-                      define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
-                    else
-                      define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
-                  fp_bs xtor_co_recs lthy
-                |>> split_list;
-
-              val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss,
-                  co_rec_sel_thmsss), fp_sugar_thms) =
+          val ((co_recs, co_rec_defs), lthy) =
+            fold_map2 (fn b =>
                 if fp = Least_FP then
-                  derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
-                    xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
-                    fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs
-                    co_rec_defs lthy
-                  |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
-                    ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
-                  ||> (fn info => (SOME info, NONE))
+                  define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
                 else
-                  derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
-                    xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs
-                    Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
-                    (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
-                    (Proof_Context.export lthy no_defs_lthy) lthy
-                  |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
-                           (corec_sel_thmsss, _)) =>
-                    (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
-                     corec_disc_thmss, corec_sel_thmsss))
-                  ||> (fn info => (NONE, SOME info));
-            in
-              (fp_res, fp_nesting_bnfs, live_nesting_bnfs, common_co_inducts, pre_bnfs, absT_infos,
-               co_recs, co_rec_defs, transpose co_inductss', co_rec_thmss, co_rec_disc_thmss,
-               co_rec_sel_thmsss, fp_sugar_thms, lthy)
-            end
-          else
-            (#fp_res fp_sugars01, [], [], #common_co_inducts fp_sugars01, map #pre_bnf fp_sugars0,
-             map #absT_info fp_sugars0, map #co_rec fp_sugars0, map #co_rec_def fp_sugars0,
-             map #co_inducts fp_sugars0, map #co_rec_thms fp_sugars0, map #co_rec_discs fp_sugars0,
-             map #co_rec_selss fp_sugars0, (NONE, NONE), no_defs_lthy);
+                  define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
+              fp_bs xtor_co_recs lthy
+            |>> split_list;
+
+          val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss,
+              co_rec_sel_thmsss), fp_sugar_thms) =
+            if fp = Least_FP then
+              derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
+                xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+                fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
+                lthy
+              |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
+                ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
+              ||> (fn info => (SOME info, NONE))
+            else
+              derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
+                xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs
+                ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
+                (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
+                (Proof_Context.export lthy no_defs_lthy) lthy
+              |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
+                       (corec_sel_thmsss, _)) =>
+                (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
+                 corec_disc_thmss, corec_sel_thmsss))
+              ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
@@ -313,8 +298,8 @@
 
         val target_fp_sugars =
           map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            co_recs co_rec_defs mapss co_inductss co_rec_thmss co_rec_disc_thmss co_rec_sel_thmsss
-            fp_sugars0;
+            co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss
+            co_rec_sel_thmsss fp_sugars0;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
@@ -340,8 +325,7 @@
 
 val impossible_caller = Bound ~1;
 
-fun nested_to_mutual_fps fp need_co_inducts_recs actual_bs actual_Ts actual_callers actual_callssss0
-    lthy =
+fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
   let
     val qsoty = quote o Syntax.string_of_typ lthy;
     val qsotys = space_implode " or " o map qsoty;
@@ -464,8 +448,8 @@
       if length perm_Tss = 1 then
         ((perm_fp_sugars0, (NONE, NONE)), lthy)
       else
-        mutualize_fp_sugars fp need_co_inducts_recs perm_cliques perm_bs perm_frozen_gen_Ts
-          perm_callers perm_callssss perm_fp_sugars0 lthy;
+        mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
+          perm_fp_sugars0 lthy;
 
     val fp_sugars = unpermute perm_fp_sugars;
   in

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 01 18:42:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 01 19:28:00 2014 +0200
@@ -377,7 +377,7 @@
 
     val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
           common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
-      nested_to_mutual_fps Greatest_FP true bs res_Ts callers callssss0 lthy0;
+      nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
 

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 18:42:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 19:28:00 2014 +0200
@@ -62,8 +62,7 @@
       map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
   end;
 
-fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref need_co_inducts_recs check_names
-    fpT_names0 lthy =
+fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref check_names fpT_names0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -146,8 +145,7 @@
 
     val ((fp_sugars, (lfp_sugar_thms, _)), lthy') =
       if nn > nn_fp then
-        mutualize_fp_sugars Least_FP need_co_inducts_recs cliques compat_bs Ts callers callssss
-          fp_sugars0 lthy
+        mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
@@ -171,16 +169,9 @@
     (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy')
   end;
 
-fun infos_of_new_datatype_mutual_cluster lthy nesting_pref fpT_name =
-  let
-    fun infos_of nesting_pref =
-      #5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy);
-  in
-    infos_of nesting_pref
-    handle ERROR _ =>
-      (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else [])
-      handle ERROR _ => []
-  end;
+fun infos_of_new_datatype_mutual_cluster lthy fpT_name =
+  #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
+  handle ERROR _ => [];
 
 fun get_all thy nesting_pref =
   let
@@ -188,23 +179,20 @@
     val old_info_tab = Old_Datatype_Data.get_all thy;
     val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
       |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
-    val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy nesting_pref) new_T_names;
+    val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
   in
     fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos
       old_info_tab
   end;
 
 fun get_one get_old get_new thy nesting_pref x =
-  let
-    val (get_fst, get_snd) =
-      (get_old thy, get_new thy nesting_pref) |> nesting_pref = Keep_Nesting ? swap
-  in
+  let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in
     (case get_fst x of NONE => get_snd x | res => res)
   end;
 
-fun get_info_of_new_datatype thy nesting_pref T_name =
+fun get_info_of_new_datatype thy T_name =
   let val lthy = Proof_Context.init_global thy in
-    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_pref T_name) T_name
+    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name
   end;
 
 val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
@@ -293,7 +281,7 @@
 fun datatype_compat fpT_names lthy =
   let
     val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
-      mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting true eq_set fpT_names lthy;
+      mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting eq_set fpT_names lthy;
 
     val all_notes =
       (case lfp_sugar_thms of

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 01 18:42:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 01 19:28:00 2014 +0200
@@ -31,7 +31,7 @@
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
           (lfp_sugar_thms, _)), lthy) =
-      nested_to_mutual_fps Least_FP true bs arg_Ts callers callssss0 lthy0;
+      nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
 
     val Ts = map #T fp_sugars;
     val Xs = map #X fp_sugars;