--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 17:06:48 2015 +0200
@@ -700,7 +700,7 @@
--| @{keyword "is"} -- Parse.term --
Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
"definition for constants over the quotient type"
(liftdef_parser >> lift_def_cmd_with_err_handling)