diff -r 67e122cedbba -r 8b159677efb5 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -97,6 +97,7 @@
 
 open BNF_Util
 open BNF_Ctr_Sugar
+open BNF_Comp
 open BNF_Def
 open BNF_FP_Util
 open BNF_FP_Def_Sugar_Tactics
@@ -1103,12 +1104,14 @@
           quote (Syntax.string_of_typ fake_lthy T)))
       | eq_fpT_check _ _ = false;
 
-    fun freeze_fp (T as Type (s, Us)) =
+    fun freeze_fp (T as Type (s, Ts)) =
         (case find_index (eq_fpT_check T) fake_Ts of
-          ~1 => Type (s, map freeze_fp Us)
+          ~1 => Type (s, map freeze_fp Ts)
         | kk => nth Xs kk)
       | freeze_fp T = T;
 
+    val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
+
     val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
 
@@ -1119,8 +1122,34 @@
            xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
            dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
            lthy)) =
-      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
-        fake_Ts fp_eqs no_defs_lthy0;
+      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
+        no_defs_lthy0
+      handle BAD_DEAD (X, X_backdrop) =>
+        (case X_backdrop of
+          Type (bad_tc, _) =>
+          let
+            val qsoty = quote o Syntax.string_of_typ fake_lthy;
+            val fake_T = qsoty (unfreeze_fp X);
+            val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
+            fun register_hint () =
+              "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^
+              quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
+              \it";
+          in
+            if is_some (bnf_of no_defs_lthy bad_tc) orelse
+               is_some (fp_sugar_of no_defs_lthy bad_tc) then
+              error ("Non-strictly-positive " ^ co_prefix fp ^ "recursive occurrence of type " ^
+                fake_T ^ " in type expression " ^ fake_T_backdrop)
+            else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+                bad_tc) then
+              error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+                " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^
+                fake_T_backdrop ^ register_hint ())
+            else
+              error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+                " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^
+                register_hint ())
+          end);
 
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());