src/HOL/Tools/choice_specification.ML
changeset 47815 43f677b3ae91
parent 46974 7ca3608146d8
child 50239 fb579401dc26
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4                               |> apfst undo_imps
     1.5                               |> apfst Drule.export_without_context
     1.6                               |-> Thm.theory_attributes
     1.7 -                                (map (Attrib.attribute thy)
     1.8 +                                (map (Attrib.attribute_cmd_global thy)
     1.9                                    (@{attributes [nitpick_choice_spec]} @ atts))
    1.10                               |> add_final
    1.11                               |> swap