# HG changeset patch
# User wenzelm
# Date 895224889 -7200
# Node ID c85b339accfe018c01e5f411c4fc5b581153bbd5
# Parent  c90411dde8e8c7de2bdd090541ab219fdc2157f5
added add_axioms_x, add_defs_x;

diff -r c90411dde8e8 -r c85b339accfe src/Pure/pure_thy.ML
--- 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 ***)