src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
 struct
 
 open BNF_Util
 open BNF_Ctr_Sugar
+open BNF_Comp
 open BNF_Def
 open BNF_FP_Util
 open BNF_FP_Def_Sugar_Tactics
 
 val EqN = "Eq_";

     fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
         s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
           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;
 
     val fp_eqs =

 
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
            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 ());
 
     val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;