src/HOL/Tools/specification_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18729 216e31270509
     1.1 --- a/src/HOL/Tools/specification_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -191,7 +191,6 @@
     1.4                          fun undo_imps thm =
     1.5                              equal_elim (symmetric rew_imp) thm
     1.6  
     1.7 -                        fun apply_atts arg = Thm.apply_attributes (arg, map (Attrib.global_attribute thy) atts)
     1.8                          fun add_final (arg as (thy, thm)) =
     1.9                              if name = ""
    1.10                              then arg |> Library.swap
    1.11 @@ -201,7 +200,7 @@
    1.12                          args |> apsnd (remove_alls frees)
    1.13                               |> apsnd undo_imps
    1.14                               |> apsnd standard
    1.15 -                             |> apply_atts
    1.16 +                             |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts)
    1.17                               |> add_final
    1.18                               |> Library.swap
    1.19                      end