src/HOL/Tools/datatype_package.ML
changeset 18708 4b3dadb4fe33
parent 18702 7dc7dcd63224
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4    val constrs_of : theory -> string -> term list option
     1.5    val case_const_of : theory -> string -> term option
     1.6    val weak_case_congs_of : theory -> thm list
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure DatatypePackage : DATATYPE_PACKAGE =
    1.12 @@ -433,8 +433,8 @@
    1.13  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
    1.14  
    1.15  val simproc_setup =
    1.16 -  [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
    1.17 -   fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
    1.18 +  Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
    1.19 +  (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
    1.20  
    1.21  
    1.22  (**** translation rules for case ****)
    1.23 @@ -545,7 +545,7 @@
    1.24      (NameSpace.accesses' case_name)) (descr ~~ case_names));
    1.25  
    1.26  val trfun_setup =
    1.27 -  [Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], [])];
    1.28 +  Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], []);
    1.29  
    1.30  
    1.31  (* prepare types *)
    1.32 @@ -1019,7 +1019,8 @@
    1.33  
    1.34  (* setup theory *)
    1.35  
    1.36 -val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup @ trfun_setup;
    1.37 +val setup =
    1.38 +  DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
    1.39  
    1.40  
    1.41  (* outer syntax *)