extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions

--- a/src/HOL/BNF_Least_Fixpoint.thy	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Mon Sep 08 14:03:01 2014 +0200
@@ -181,6 +181,50 @@
 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   by (rule ssubst)
 
+lemma all_mem_range1:
+  "(\<And>y. y \<in> range f \<Longrightarrow> P y) \<equiv> (\<And>x. P (f x)) "
+  by (rule equal_intr_rule) fast+
+
+lemma all_mem_range2:
+  "(\<And>fa y. fa \<in> range f \<Longrightarrow> y \<in> range fa \<Longrightarrow> P y) \<equiv> (\<And>x xa. P (f x xa))"
+  by (rule equal_intr_rule) fast+
+
+lemma all_mem_range3:
+  "(\<And>fa fb y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> y \<in> range fb \<Longrightarrow> P y) \<equiv> (\<And>x xa xb. P (f x xa xb))"
+  by (rule equal_intr_rule) fast+
+
+lemma all_mem_range4:
+  "(\<And>fa fb fc y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> fc \<in> range fb \<Longrightarrow> y \<in> range fc \<Longrightarrow> P y) \<equiv>
+   (\<And>x xa xb xc. P (f x xa xb xc))"
+  by (rule equal_intr_rule) fast+
+
+lemma all_mem_range5:
+  "(\<And>fa fb fc fd y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> fc \<in> range fb \<Longrightarrow> fd \<in> range fc \<Longrightarrow>
+     y \<in> range fd \<Longrightarrow> P y) \<equiv>
+   (\<And>x xa xb xc xd. P (f x xa xb xc xd))"
+  by (rule equal_intr_rule) fast+
+
+lemma all_mem_range6:
+  "(\<And>fa fb fc fd fe ff y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> fc \<in> range fb \<Longrightarrow> fd \<in> range fc \<Longrightarrow>
+     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> y \<in> range ff \<Longrightarrow> P y) \<equiv>
+   (\<And>x xa xb xc xd xe xf. P (f x xa xb xc xd xe xf))"
+  by (rule equal_intr_rule) (fastforce, fast)
+
+lemma all_mem_range7:
+  "(\<And>fa fb fc fd fe ff fg y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> fc \<in> range fb \<Longrightarrow> fd \<in> range fc \<Longrightarrow>
+     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> fg \<in> range ff \<Longrightarrow> y \<in> range fg \<Longrightarrow> P y) \<equiv>
+   (\<And>x xa xb xc xd xe xf xg. P (f x xa xb xc xd xe xf xg))"
+  by (rule equal_intr_rule) (fastforce, fast)
+
+lemma all_mem_range8:
+  "(\<And>fa fb fc fd fe ff fg fh y. fa \<in> range f \<Longrightarrow> fb \<in> range fa \<Longrightarrow> fc \<in> range fb \<Longrightarrow> fd \<in> range fc \<Longrightarrow>
+     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> fg \<in> range ff \<Longrightarrow> fh \<in> range fg \<Longrightarrow> y \<in> range fh \<Longrightarrow> P y) \<equiv>
+   (\<And>x xa xb xc xd xe xf xg xh. P (f x xa xb xc xd xe xf xg xh))"
+  by (rule equal_intr_rule) (fastforce, fast)
+
+lemmas all_mem_range = all_mem_range1 all_mem_range2 all_mem_range3 all_mem_range4 all_mem_range5
+  all_mem_range6 all_mem_range7 all_mem_range8
+
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -536,7 +536,7 @@
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst);
+    val cst' = mk_co_rec thy fp Cs fpT (Morphism.term phi cst);
     val def' = Morphism.thm phi def;
   in
     ((cst', def'), lthy')
@@ -1464,7 +1464,7 @@
               sel_default_eqs) lthy
           end;
 
-        fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
+        fun derive_map_set_rel_thms (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
             exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss,
             ...} : ctr_sugar, lthy) =
           if live = 0 then
@@ -1989,7 +1989,7 @@
           (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
       in
         (wrap_ctrs
-         #> derive_maps_sets_rels
+         #> derive_map_set_rel_thms
          ##>>
            (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
            else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -227,58 +227,56 @@
 
         val fp_absT_infos = map #absT_info fp_sugars0;
 
-          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 pre = Binding.prefix_name (pre ^ "_") 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 ((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) =
-            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 ((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;
 

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -37,7 +37,7 @@
   val mk_compN: int -> typ list -> term * term -> term
   val mk_comp: typ list -> term * term -> term
 
-  val mk_co_rec: theory -> fp_kind -> typ -> typ list -> term -> term
+  val mk_co_rec: theory -> fp_kind -> typ list -> typ -> term -> term
 
   val mk_conjunctN: int -> int -> thm
   val conj_dests: int -> thm -> thm list
@@ -105,7 +105,7 @@
 
 val mk_comp = mk_compN 1;
 
-fun mk_co_rec thy fp fpT Cs t =
+fun mk_co_rec thy fp Cs fpT t =
   let
     val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
     val fpT0 = case_fp fp prebody body;

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -462,7 +462,7 @@
     fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
         co_rec_thms = corec_thms, co_rec_discs = corec_discs,
         co_rec_selss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
-      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
+      {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
        sel_defs = sel_defs,
        fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
        fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -43,15 +43,152 @@
 
 open Ctr_Sugar
 open BNF_Util
+open BNF_Tactics
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
 open BNF_LFP
 
-val compatN = "compat_";
+val compat_N = "compat_";
+val rec_fun_N = "rec_fun_";
 
 datatype nesting_preference = Keep_Nesting | Unfold_Nesting;
 
+fun mk_fun_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) =
+  let
+    fun repair_rec_arg_args [] [] = []
+      | repair_rec_arg_args ((g_T as Type (@{type_name fun}, _)) :: g_Ts) (g :: gs) =
+        let
+          val (x_Ts, body_T) = strip_type g_T;
+        in
+          (case try HOLogic.dest_prodT body_T of
+            NONE => [g]
+          | SOME (fst_T, _) =>
+            if member (op =) fpTs fst_T then
+              let val (xs, _) = mk_Frees "x" x_Ts ctxt in
+                map (fn mk_proj => fold_rev Term.lambda xs (mk_proj (Term.list_comb (g, xs))))
+                  [HOLogic.mk_fst, HOLogic.mk_snd]
+              end
+            else
+              [g])
+          :: repair_rec_arg_args g_Ts gs
+        end
+      | repair_rec_arg_args (g_T :: g_Ts) (g :: gs) =
+        if member (op =) fpTs g_T then
+          let
+            val j = find_index (member (op =) Cs) g_Ts;
+            val h = nth gs j;
+            val g_Ts' = nth_drop j g_Ts;
+            val gs' = nth_drop j gs;
+          in
+            [g, h] :: repair_rec_arg_args g_Ts' gs'
+          end
+        else
+          [g] :: repair_rec_arg_args g_Ts gs;
+
+    fun repair_back_rec_arg f_T f' =
+      let
+        val g_Ts = Term.binder_types f_T;
+        val (gs, _) = mk_Frees "g" g_Ts ctxt;
+      in
+        fold_rev Term.lambda gs (Term.list_comb (f',
+          flat_rec_arg_args (repair_rec_arg_args g_Ts gs)))
+      end;
+
+    val f_Ts = binder_fun_types (fastype_of rec1);
+    val (fs', _) = mk_Frees "f" (replicate (length f_Ts) Term.dummyT) ctxt;
+
+    fun mk_rec' recx =
+      fold_rev Term.lambda fs' (Term.list_comb (recx, map2 repair_back_rec_arg f_Ts fs'))
+      |> Syntax.check_term ctxt;
+  in
+    map mk_rec' recs
+  end;
+
+fun define_fun_recs fpTs Cs recs lthy =
+  let
+    val b_names = Name.variant_list [] (map base_name_of_typ fpTs);
+
+    fun mk_binding b_name =
+      Binding.qualify true (compat_N ^ b_name)
+        (Binding.prefix_name rec_fun_N (Binding.name b_name));
+
+    val bs = map mk_binding b_names;
+    val rhss = mk_fun_rec_rhs lthy fpTs Cs recs;
+  in
+    fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy
+  end;
+
+fun mk_fun_rec_thmss ctxt rec0_thmss (recs as rec1 :: _) rec_defs =
+  let
+    val f_Ts = binder_fun_types (fastype_of rec1);
+    val (fs, _) = mk_Frees "f" f_Ts ctxt;
+    val frecs = map (fn recx => Term.list_comb (recx, fs)) recs;
+
+    fun mk_ctrs_of (Type (T_name, As)) =
+      map (mk_ctr As) (#ctrs (the (ctr_sugar_of ctxt T_name)));
+
+    val fpTs = map (domain_type o body_fun_type o fastype_of) recs;
+    val fpTs_frecs = fpTs ~~ frecs;
+    val ctrss = map mk_ctrs_of fpTs;
+    val fss = unflat ctrss fs;
+
+    fun mk_rec_call g n (Type (@{type_name fun}, [dom_T, ran_T])) =
+        Abs (Name.uu, dom_T, mk_rec_call g (n + 1) ran_T)
+      | mk_rec_call g n fpT =
+        let
+          val frec = the (AList.lookup (op =) fpTs_frecs fpT);
+          val xg = Term.list_comb (g, map Bound (n - 1 downto 0));
+        in frec $ xg end;
+
+    fun mk_rec_arg_arg g_T g =
+      g :: (if exists_subtype_in fpTs g_T then [mk_rec_call g 0 g_T] else []);
+
+    fun mk_goal frec ctr f =
+      let
+        val g_Ts = binder_types (fastype_of ctr);
+        val (gs, _) = mk_Frees "g" g_Ts ctxt;
+        val gctr = Term.list_comb (ctr, gs);
+        val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg g_Ts gs);
+      in
+        fold_rev (fold_rev Logic.all) [fs, gs]
+          (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs)))
+      end;
+
+    fun mk_goals ctrs fs frec = map2 (mk_goal frec) ctrs fs;
+
+    val goalss = map3 mk_goals ctrss fss frecs;
+
+    fun tac ctxt =
+      unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN
+      HEADGOAL (rtac refl);
+
+    fun prove goal =
+      Goal.prove_sorry ctxt [] [] goal (tac o #context)
+      |> Thm.close_derivation;
+  in
+    map (map prove) goalss
+  end;
+
+fun define_fun_rec_derive_thms induct inducts recs0 rec_thmss fpTs lthy =
+  let
+    val thy = Proof_Context.theory_of lthy;
+
+    (* imperfect: will not yield the expected theorem for functions taking a large number of
+       arguments *)
+    val repair_induct = unfold_thms lthy @{thms all_mem_range};
+
+    val induct' = repair_induct induct;
+    val inducts' = map repair_induct inducts;
+
+    val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0;
+    val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0;
+    val ((recs', rec'_defs), lthy') = define_fun_recs fpTs Cs recs lthy |>> split_list;
+    val rec'_thmss = mk_fun_rec_thmss lthy' rec_thmss recs' rec'_defs;
+  in
+    ((induct', inducts', recs', rec'_thmss), lthy')
+  end;
+
 fun reindex_desc desc =
   let
     val kks = map fst desc;
@@ -130,10 +267,10 @@
 
     val dest_dtyp = Old_Datatype_Aux.typ_of_dtyp descr;
 
-    val Ts = Old_Datatype_Aux.get_rec_types descr;
-    val nn = length Ts;
+    val fpTs' = Old_Datatype_Aux.get_rec_types descr;
+    val nn = length fpTs';
 
-    val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
+    val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) fpTs';
     val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr;
     val kkssss =
       map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr;
@@ -146,34 +283,47 @@
     val callssss =
       map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss;
 
-    val b_names = Name.variant_list [] (map base_name_of_typ Ts);
-    val compat_b_names = map (prefix compatN) b_names;
+    val b_names = Name.variant_list [] (map base_name_of_typ fpTs');
+    val compat_b_names = map (prefix compat_N) b_names;
     val compat_bs = map Binding.name compat_b_names;
 
     val ((fp_sugars, (lfp_sugar_thms, _)), lthy') =
       if nn > nn_fp then
-        mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy
+        mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars0 lthy
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
-    val recs = map (fst o dest_Const o #co_rec) fp_sugars;
-    val rec_thms = maps #co_rec_thms fp_sugars;
-
     val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
     val inducts = map (the_single o #co_inducts) fp_sugars;
 
+    val recs = map #co_rec fp_sugars;
+    val rec_thmss = map #co_rec_thms fp_sugars;
+
+    fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) fpTs' (body_type T)
+      | is_nested_rec_type _ = false;
+
+    val ((induct', inducts', recs', rec'_thmss), lthy'') =
+      if nesting_pref = Unfold_Nesting andalso
+         exists (exists (exists is_nested_rec_type)) ctr_Tsss then
+        define_fun_rec_derive_thms induct inducts recs rec_thmss fpTs' lthy'
+      else
+        ((induct, inducts, recs, rec_thmss), lthy');
+
+    val rec'_names = map (fst o dest_Const) recs';
+    val rec'_thms = flat rec'_thmss;
+
     fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
         distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
       (T_name0,
-       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
-        inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
-        rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct',
+        inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names,
+        rec_rewrites = rec'_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
         case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
         split_asm = split_asm});
 
     val infos = map_index mk_info (take nn_fp fp_sugars);
   in
-    (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy')
+    (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy'')
   end;
 
 fun infos_of_new_datatype_mutual_cluster lthy fpT_name =
@@ -298,7 +448,7 @@
         NONE => []
       | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
         let
-          val common_name = compatN ^ mk_common_name b_names;
+          val common_name = compat_N ^ mk_common_name b_names;
 
           val common_notes =
             (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -194,7 +194,7 @@
 
     fun mk_spec ctr_offset
         ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
-      {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
+      {recx = mk_co_rec thy Least_FP perm_Cs' (substAT T) recx,
        fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
        ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
   in

--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -331,7 +331,8 @@
     fun get_dt_descr T i tname dts =
       (case Symtab.lookup dt_info tname of
         NONE =>
-          typ_error T (quote tname ^ " is not a datatype - can't use it in nested recursion")
+          typ_error T (quote tname ^ " is not registered as an old-style datatype and hence cannot \
+            \be used in nested recursion")
       | SOME {index, descr, ...} =>
           let
             val (_, vars, _) = the (AList.lookup (op =) descr index);