--- 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
--- 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')
--- 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
--- 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 _ =