1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 09:39:10 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 09:40:11 2010 +0100
     1.3 @@ -238,10 +238,14 @@
     1.4      |> split_list_kind thy o Termtab.dest
     1.5  in
     1.6  fun add_axioms verbose axs thy =
     1.7 -  let val (used, new) = mark_axioms thy (name_axioms axs)
     1.8 +  let
     1.9 +    val (used, new) = mark_axioms thy (name_axioms axs)
    1.10 +    fun add (n, t) =
    1.11 +      Specification.axiomatization [] [((Binding.name n, []), [t])] #>>
    1.12 +      hd o hd o snd
    1.13    in
    1.14      thy
    1.15 -    |> fold_map (Drule.add_axiom o apfst Binding.name) new
    1.16 +    |> fold_map add new
    1.17      |-> Context.theory_map o fold Boogie_Axioms.add_thm
    1.18      |> log verbose "The following axioms were added:" (map fst new)
    1.19      |> (fn thy' => log verbose "The following axioms already existed:"