1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 14:17:41 2011 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5      val (((def1, def2), def3), lthy) = thy |>
     1.6  
     1.7 -      Class.instantiation ([tyname'], [], @{sort enum}) |>
     1.8 +      Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
     1.9  
    1.10        define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
    1.11          (p,
    1.12 @@ -266,7 +266,7 @@
    1.13    in
    1.14      lthy' |>
    1.15      Local_Theory.note
    1.16 -      ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
    1.17 +      ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>
    1.18      Local_Theory.note
    1.19        ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
    1.20      Local_Theory.note