diff -r e7d004b89ca8 -r f81557a124d5 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Mar 21 22:24:04 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Mon Mar 22 00:48:56 2010 +0100
@@ -44,9 +44,9 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
+                    val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy
                 in
-                    (thy',hd thms)
+                    (thy', thm)
                 end
               | process ((thname,cname,covld)::cos) (thy,tm) =
                 case tm of