# HG changeset patch
# User wenzelm
# Date 1236864623 -3600
# Node ID 9ae8f9d78cd3b61021c2276f53e21a7f76461cae
# Parent  de9e8f1d927c673ed1e84b49aebbae08ee7be526
axiomatization: more precise treatment of binding;

diff -r de9e8f1d927c -r 9ae8f9d78cd3 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 12 13:18:42 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 12 14:30:23 2009 +0100
@@ -147,12 +147,16 @@
     val subst = Term.subst_atomic (map Free xs ~~ consts);
 
     (*axioms*)
-    val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom  (* FIXME proper use of binding!? *)
-          ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
+    val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
+        fold_map Thm.add_axiom
+          (map (apfst (fn a => Binding.map_name (K a) b))
+            (PureThy.name_multi (Binding.name_of b) (map subst props)))
+        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
+
+    (*facts*)
     val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
+
     val _ =
       if not do_print then ()
       else print_consts (ProofContext.init thy') (K false) xs;