more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 14 10:55:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 14 11:07:59 2013 +0200
@@ -1496,6 +1496,12 @@
            (unfoldN, unfold_thmss, K coiter_attrs)]
           |> massage_multi_notes;
 
+        fun is_codatatype (Type (s, _)) =
+            (case fp_sugar_of lthy s of SOME {fp = Greatest_FP, ...} => true | _ => false)
+          | is_codatatype _ = false;
+
+        val nitpick_supported = forall (is_codatatype o T_of_bnf) nested_bnfs;
+
         fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
           Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
             (map (dest_Const o mk_ctr As) ctrs)
@@ -1507,7 +1513,7 @@
           ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
           (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
           (transpose [sel_unfold_thmsss, sel_corec_thmsss])
-        |> fold2 register_nitpick fpTs ctr_sugars
+        |> nitpick_supported ? fold2 register_nitpick fpTs ctr_sugars
       end;
 
     val lthy'' = lthy'