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