src/HOL/Tools/record_package.ML
changeset 18708 4b3dadb4fe33
parent 18688 abf0f018b5ec
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/record_package.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4      -> theory -> theory
     1.5    val add_record_i: string list * string -> (typ list * string) option
     1.6      -> (string * typ * mixfix) list -> theory -> theory
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -2098,11 +2098,11 @@
    1.13  (* setup theory *)
    1.14  
    1.15  val setup =
    1.16 - [RecordsData.init,
    1.17 -  Theory.add_trfuns ([], parse_translation, [], []),
    1.18 -  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
    1.19 +  RecordsData.init #>
    1.20 +  Theory.add_trfuns ([], parse_translation, [], []) #>
    1.21 +  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
    1.22    (fn thy => (Simplifier.change_simpset_of thy
    1.23 -    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
    1.24 +    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
    1.25  
    1.26  (* outer syntax *)
    1.27