# HG changeset patch
# User blanchet
# Date 1472733524 -7200
# Node ID 622b54bbe8d4d9c98265cd2450630356f1854f6e
# Parent  9f906a2eb0e70d6d93d985c363765431e7328308
more robustness

diff -r 9f906a2eb0e7 -r 622b54bbe8d4 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Sep 01 12:10:52 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Sep 01 14:38:44 2016 +0200
@@ -221,7 +221,7 @@
     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;
 
@@ -237,7 +237,8 @@
     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) =
@@ -310,11 +311,13 @@
       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;