# HG changeset patch
# User wenzelm
# Date 1269282314 -3600
# Node ID 387de5db0a74a8e5b17a9b15061ba016ee0ce061
# Parent  ab6dc4d86ea11edd3355480ab06a64cd7b7cc179
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);

diff -r ab6dc4d86ea1 -r 387de5db0a74 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 19:23:03 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 19:25:14 2010 +0100
@@ -240,13 +240,10 @@
 fun add_axioms verbose axs thy =
   let
     val (used, new) = mark_axioms thy (name_axioms axs)
-    fun add (n, t) =
-      Specification.axiomatization [] [((Binding.name n, []), [t])] #>>
-      hd o hd o snd
   in
     thy
-    |> fold_map add new
-    |-> Context.theory_map o fold Boogie_Axioms.add_thm
+    |> fold_map (fn (n, t) => Specification.axiom ((Binding.name n, []), t)) new
+    |-> Context.theory_map o fold (Boogie_Axioms.add_thm o Drule.export_without_context)
     |> log verbose "The following axioms were added:" (map fst new)
     |> (fn thy' => log verbose "The following axioms already existed:"
          (map (Display.string_of_thm_global thy') used) thy')