--- a/src/Pure/pure_thy.ML Fri May 15 11:34:12 1998 +0200
+++ b/src/Pure/pure_thy.ML Fri May 15 11:34:49 1998 +0200
@@ -24,10 +24,12 @@
val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory
val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory
val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_axioms_x: ((bstring * string) * tag list) list -> theory -> theory
val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory
val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory
val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory
val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_defs_x: ((bstring * string) * tag list) list -> theory -> theory
val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory
val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
@@ -269,6 +271,9 @@
val add_defss_i = add_axs name_multi Theory.add_defs_i;
end;
+fun add_axioms_x axms thy = add_axioms (map (apsnd (map (Attribute.global_attr thy))) axms) thy;
+fun add_defs_x defs thy = add_defs (map (apsnd (map (Attribute.global_attr thy))) defs) thy;
+
(*** add logical types ***)