--- a/src/HOL/Tools/inductive_codegen.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon May 17 23:54:15 2010 +0200
@@ -775,7 +775,7 @@
add_codegen "inductive" inductive_codegen #>
Attrib.setup @{binding code_ind}
(Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
"introduction rules for executable predicates";
(**** Quickcheck involving inductive predicates ****)