src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

           Type (bad_tc, _) =>
           let
             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 " ^
+              "\nUse the " ^ quote (#1 @{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