changeset 55111 | 5792f5106c40 |
parent 54883 | dd04a8b654fc |
child 55997 | 9dc5ce83202c |
--- a/src/HOL/Tools/inductive.ML Wed Jan 22 15:28:19 2014 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Jan 22 16:03:11 2014 +0100 @@ -591,7 +591,7 @@ val ind_cases_setup = Method.setup @{binding ind_cases} - (Scan.lift (Scan.repeat1 Args.name_source -- + (Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >> (fn (raw_props, fixes) => fn ctxt => let