--- 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