diff -r 4e8899357971 -r 8baa0b7f3f66 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Nov 19 17:20:17 2011 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sat Nov 19 21:18:38 2011 +0100
@@ -194,8 +194,9 @@
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
                              |> apsnd Drule.export_without_context
-                             |> Thm.theory_attributes (map (Attrib.attribute thy)
-                                                           (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts))
+                             |> Thm.theory_attributes
+                                (map (Attrib.attribute thy)
+                                  (@{attributes [nitpick_choice_spec]} @ atts))
                              |> add_final
                              |> Library.swap
                     end