# HG changeset patch
# User wenzelm
# Date 1466523345 -7200
# Node ID 49fa6aaa4529bd4574cc8a1ba8e2cff9a4223c01
# Parent  40f58bb9c846ff012ee0e8f07191928012963bf3
tuned;

diff -r 40f58bb9c846 -r 49fa6aaa4529 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- 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
diff -r 40f58bb9c846 -r 49fa6aaa4529 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 21 17:25:28 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 21 17:35:45 2016 +0200
@@ -810,7 +810,7 @@
 (* command syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword "lift_definition"}
+  Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
     "definition for constants over the quotient type"
     (parse_params --
       (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
diff -r 40f58bb9c846 -r 49fa6aaa4529 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Jun 21 17:25:28 2016 +0200
+++ b/src/HOL/Tools/record.ML	Tue Jun 21 17:35:45 2016 +0200
@@ -2415,7 +2415,7 @@
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
 
 val _ =
-  Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
+  Outer_Syntax.command @{command_keyword print_record} "print record definiton"
     (opt_modes -- Parse.typ >> print_record);
 
 end
diff -r 40f58bb9c846 -r 49fa6aaa4529 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Jun 21 17:25:28 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Jun 21 17:35:45 2016 +0200
@@ -869,7 +869,7 @@
     (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
-  Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)"
+  Outer_Syntax.command @{command_keyword \<proof>} "dummy proof (quick-and-dirty mode only!)"
     (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =