--- a/src/HOL/Tools/inductive.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 13 18:01:05 2016 +0200
@@ -1182,7 +1182,7 @@
fun gen_ind_decl mk_def coind =
Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
>> (fn (((preds, params), specs), monos) =>
(snd o gen_add_inductive mk_def true coind preds params specs monos));