changeset 27809 | a1e409db516b |
parent 27398 | 768da1da59d6 |
child 28537 | 1e84256d1a8a |
--- a/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 12:28:13 2008 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 22:43:46 2008 +0200 @@ -697,6 +697,6 @@ val setup = add_codegen "inductive" inductive_codegen #> Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- - Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add); + Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add); end;