src/HOL/Tools/BNF/bnf_lfp_compat.ML

       | NONE => not_datatype s);
 
     val fpTs0 as Type (_, var_As) :: _ =
       map (#T o checked_fp_sugar_of o fst o dest_Type)
         (#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
-    val fpT_names = map (fst o dest_Type) fpTs0;
+    val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0;
 
     val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
 
     val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy;
     val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;

 
     fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp);
     fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
       (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
 
-    val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
+    val fp_sugars as {fp, ...} :: _ = map checked_fp_sugar_of fpT_names;
+    val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
     val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
     val all_infos = Old_Datatype_Data.get_all thy;
     val (orig_descr' :: nested_descrs) =
       if member (op =) prefs Keep_Nesting then [orig_descr]
       else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp);

 
     val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') =
       if member (op =) prefs Keep_Nesting orelse
          not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then
         ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy')
-      else
+      else if fp = Least_FP then
         define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs
           rec_thmss lthy'
         |>> `(fn (inducts', induct', _, rec'_thmss) =>
-          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])));
+          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])))
+      else
+        not_datatype fpT_name1;
 
     val rec'_names = map (fst o dest_Const) recs';
     val rec'_thms = flat rec'_thmss;
 
     fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy,