src/Pure/Isar/isar_thy.ML
changeset 8428 be4c8a57cf7e
parent 8371 7313627803f4
child 8450 dc44d6533f0f
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:43 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:57 2000 +0100
     1.3 @@ -216,10 +216,10 @@
     1.4  fun add_axms f args thy =
     1.5    f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
     1.6  
     1.7 -val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore;
     1.8 -val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore;
     1.9 -val add_defs = add_axms PureThy.add_defs o map Comment.ignore;
    1.10 -val add_defs_i = PureThy.add_defs_i o map Comment.ignore;
    1.11 +val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
    1.12 +val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
    1.13 +val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore;
    1.14 +val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore;
    1.15  
    1.16  
    1.17  (* constdefs *)