| changeset 63285 | e9c777bfd78c |
| parent 63180 | ddfd021884b4 |
| child 63395 | 734723445a8c |
--- a/src/HOL/Tools/inductive.ML Sat Jun 11 13:57:59 2016 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Jun 11 16:41:11 2016 +0200 @@ -1169,7 +1169,7 @@ (** outer syntax **) fun gen_ind_decl mk_def coind = - Parse.fixes -- Parse.for_fixes -- + Parse.vars -- Parse.for_fixes -- Scan.optional Parse_Spec.where_multi_specs [] -- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] >> (fn (((preds, params), specs), monos) =>