# HG changeset patch
# User wenzelm
# Date 939211431 -7200
# Node ID c9e7b053694a6848a9e805f12f42ba952b0f2fb6
# Parent  7ee322caf59cb2d63d5d578a4e4e602f17c9bbcb
fixed naming of single axioms;

diff -r 7ee322caf59c -r c9e7b053694a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Oct 06 00:35:05 1999 +0200
+++ b/src/Pure/pure_thy.ML	Wed Oct 06 14:03:51 1999 +0200
@@ -271,23 +271,33 @@
 (* store axioms as theorems *)
 
 local
-  fun add_ax app_name add ((name, axs), atts) thy =
+  fun get_axs thy named_axs = map (Thm.get_axiom thy o fst) named_axs;
+
+  fun add_single add ((name, ax), atts) thy =
     let
-      val named_axs = app_name name axs;
+      val named_ax = name_single name ax;
+      val thy' = add named_ax thy;
+      val thm = hd (get_axs thy' named_ax);
+    in add_thms [((name, thm), atts)] thy' end;
+
+  fun add_multi add ((name, axs), atts) thy =
+    let
+      val named_axs = name_multi name axs;
       val thy' = add named_axs thy;
-      val thms = map (Thm.get_axiom thy' o fst) named_axs;
+      val thms = get_axs thy' named_axs;
     in add_thmss [((name, thms), atts)] thy' end;
 
-  fun add_axs app_name add = Library.apply o map (add_ax app_name add);
+  fun add_singles add = Library.apply o map (add_single add);
+  fun add_multis add = Library.apply o map (add_multi add);
 in
-  val add_axioms    = add_axs name_single Theory.add_axioms;
-  val add_axioms_i  = add_axs name_single Theory.add_axioms_i;
-  val add_axiomss   = add_axs name_multi Theory.add_axioms;
-  val add_axiomss_i = add_axs name_multi Theory.add_axioms_i;
-  val add_defs      = add_axs name_single Theory.add_defs;
-  val add_defs_i    = add_axs name_single Theory.add_defs_i;
-  val add_defss     = add_axs name_multi Theory.add_defs;
-  val add_defss_i   = add_axs name_multi Theory.add_defs_i;
+  val add_axioms    = add_singles Theory.add_axioms;
+  val add_axioms_i  = add_singles Theory.add_axioms_i;
+  val add_axiomss   = add_multis Theory.add_axioms;
+  val add_axiomss_i = add_multis Theory.add_axioms_i;
+  val add_defs      = add_singles Theory.add_defs;
+  val add_defs_i    = add_singles Theory.add_defs_i;
+  val add_defss     = add_multis Theory.add_defs;
+  val add_defss_i   = add_multis Theory.add_defs_i;
 end;