src/HOL/Tools/BNF/bnf_lfp_compat.ML

 
 fun mk_infos_of_mutually_recursive_new_datatypes prefs check_names fpT_names0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
-    fun not_datatype s = error (quote s ^ " is not a datatype");
+    fun not_datatype_name s =
+      error (quote s ^ " is not a datatype");
     fun not_mutually_recursive ss =
       error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
 
     fun checked_fp_sugar_of s =
       (case fp_sugar_of lthy s of
         SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) =>
-        if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s
-      | _ => not_datatype s);
+        if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar
+        else not_datatype_name s
+      | _ => not_datatype_name 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 as fpT_name1 :: _ = map (fst o dest_Type) fpTs0;

         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, [])))
       else
-        not_datatype fpT_name1;
+        not_datatype_name 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,