1.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 19 14:17:41 2011 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  text {* Enumeration types *}
     1.6  
     1.7 -class enum = ord + finite +
     1.8 +class spark_enum = ord + finite +
     1.9    fixes pos :: "'a \<Rightarrow> int"
    1.10    assumes range_pos: "range pos = {0..<int (card (UNIV::'a set))}"
    1.11    and less_pos: "(x < y) = (pos x < pos y)"

     2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 12:22:59 2011 +0200
     2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 14:17:41 2011 +0200
     2.3 @@ -176,7 +176,7 @@
     2.4  
     2.5      val (((def1, def2), def3), lthy) = thy |>
     2.6  
     2.7 -      Class.instantiation ([tyname'], [], @{sort enum}) |>
     2.8 +      Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
     2.9  
    2.10        define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
    2.11          (p,
    2.12 @@ -266,7 +266,7 @@
    2.13    in
    2.14      lthy' |>
    2.15      Local_Theory.note
    2.16 -      ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
    2.17 +      ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>
    2.18      Local_Theory.note
    2.19        ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
    2.20      Local_Theory.note