# HG changeset patch
# User boehmes
# Date 1269247211 -3600
# Node ID c2039b00ff0d8e5248c996cb348173435cb54db2
# Parent  6b4e3b2d33b02d75c814d878b75835d53c7b2b86
replaced old-style Drule.add_axiom by Specification.axiomatization

diff -r 6b4e3b2d33b0 -r c2039b00ff0d src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 09:39:10 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 09:40:11 2010 +0100
@@ -238,10 +238,14 @@
     |> split_list_kind thy o Termtab.dest
 in
 fun add_axioms verbose axs thy =
-  let val (used, new) = mark_axioms thy (name_axioms axs)
+  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 (Drule.add_axiom o apfst Binding.name) new
+    |> fold_map add new
     |-> Context.theory_map o fold Boogie_Axioms.add_thm
     |> log verbose "The following axioms were added:" (map fst new)
     |> (fn thy' => log verbose "The following axioms already existed:"