1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 17:20:17 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 21:18:38 2011 +0100
     1.3 @@ -260,21 +260,18 @@
     1.4           (Const (@{const_name last_el}, T), List.last cs)))
     1.5        (fn _ => simp_tac (simpset_of lthy' addsimps
     1.6           [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
     1.7 -
     1.8 -    val simp_att = [Attrib.internal (K Simplifier.simp_add)]
     1.9 -
    1.10    in
    1.11      lthy' |>
    1.12      Local_Theory.note
    1.13 -      ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>
    1.14 +      ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>
    1.15      Local_Theory.note
    1.16 -      ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
    1.17 +      ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>
    1.18      Local_Theory.note
    1.19 -      ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
    1.20 +      ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>
    1.21      Local_Theory.note
    1.22 -      ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
    1.23 +      ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>
    1.24      Local_Theory.note
    1.25 -      ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
    1.26 +      ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>
    1.27      Local_Theory.exit_global
    1.28    end;
    1.29