# HG changeset patch
# User wenzelm
# Date 897472660 -7200
# Node ID b4bd7e6402fe578c764eaabfe9bbcc10a6042ee6
# Parent  235f8508d4406af77fe5ffb8d80a6368e03a2ff5
moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;

diff -r 235f8508d440 -r b4bd7e6402fe src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jun 10 11:57:01 1998 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jun 10 11:57:40 1998 +0200
@@ -27,12 +27,10 @@
   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 get_name: theory -> string
@@ -281,9 +279,6 @@
   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;
-
 
 
 (*** derived theory operations ***)
@@ -382,7 +377,7 @@
 
 val proto_pure =
   Theory.pre_pure
-  |> Theory.apply (Attribute.setup @ [TheoremsData.init, TheoryManagementData.init])
+  |> Theory.apply [TheoremsData.init, TheoryManagementData.init]
   |> put_name "ProtoPure"
   |> global_path
   |> Theory.add_types