src/HOL/Tools/recfun_codegen.ML
changeset 18708 4b3dadb4fe33
parent 18702 7dc7dcd63224
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val del: theory attribute
     1.5    val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
     1.6    val get_thm_equations: theory -> string * typ -> (thm list * typ) option
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure RecfunCodegen : RECFUN_CODEGEN =
    1.12 @@ -191,14 +191,13 @@
    1.13    | _ => NONE);
    1.14  
    1.15  
    1.16 -val setup = [
    1.17 -  CodegenData.init,
    1.18 -  add_codegen "recfun" recfun_codegen,
    1.19 +val setup =
    1.20 +  CodegenData.init #>
    1.21 +  add_codegen "recfun" recfun_codegen #>
    1.22    add_attribute ""
    1.23      (   Args.del |-- Scan.succeed del
    1.24 -     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
    1.25 +     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add) #>
    1.26    CodegenPackage.add_eqextr
    1.27 -    ("rec", fn thy => fn _ => get_thm_equations thy)
    1.28 -];
    1.29 +    ("rec", fn thy => fn _ => get_thm_equations thy);
    1.30  
    1.31  end;