| changeset 24219 | e558fe311376 |
| parent 24129 | 591394d9ee66 |
| child 24458 | 83b6119078bc |
--- a/src/HOL/Tools/inductive_codegen.ML Fri Aug 10 17:04:24 2007 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Aug 10 17:04:34 2007 +0200 @@ -697,7 +697,7 @@ val setup = add_codegen "inductive" inductive_codegen #> - add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- + Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add); end;