--- a/src/HOL/Tools/inductive.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Mar 15 20:07:00 2012 +0100
@@ -1137,7 +1137,7 @@
fun gen_ind_decl mk_def coind =
Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
(snd oo gen_add_inductive mk_def true coind preds params specs monos));