src/HOL/Tools/inductive_codegen.ML
changeset 18708 4b3dadb4fe33
parent 18388 ab1a710a68ce
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature INDUCTIVE_CODEGEN =
     1.5  sig
     1.6    val add : string option -> theory attribute
     1.7 -  val setup : (theory -> theory) list
     1.8 +  val setup : theory -> theory
     1.9  end;
    1.10  
    1.11  structure InductiveCodegen : INDUCTIVE_CODEGEN =
    1.12 @@ -732,10 +732,9 @@
    1.13      | _ => NONE);
    1.14  
    1.15  val setup =
    1.16 -  [add_codegen "inductive" inductive_codegen,
    1.17 -   CodegenData.init,
    1.18 -   add_attribute "ind"
    1.19 -     (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
    1.20 +  add_codegen "inductive" inductive_codegen #>
    1.21 +  CodegenData.init #>
    1.22 +  add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
    1.23  
    1.24  end;
    1.25