--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Tue Jun 21 17:25:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Tue Jun 21 17:35:45 2016 +0200
@@ -525,7 +525,7 @@
val T = qsoty (unfreeze_fp Y);
val T_backdrop = qsoty (unfreeze_fp Y_backdrop);
fun register_hint () =
- "\nUse the " ^ quote (#1 @{command_keyword "bnf"}) ^ " command to register " ^
+ "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
\it";
in