# HG changeset patch
# User berghofe
# Date 1303215461 -7200
# Node ID a8a9f4d79196f6d55275e868f4eafeb57e5abaa1
# Parent  9465651c0db7175cff201162126f5f047a6f809b
- renamed enum type class to spark_enum, to avoid confusion with
  enum type class defined in Enum theory
- renamed theorem ..._card_UNIV to ..._card

diff -r 9465651c0db7 -r a8a9f4d79196 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 19 14:17:41 2011 +0200
@@ -69,7 +69,7 @@
 
 text {* Enumeration types *}
 
-class enum = ord + finite +
+class spark_enum = ord + finite +
   fixes pos :: "'a \<Rightarrow> int"
   assumes range_pos: "range pos = {0..<int (card (UNIV::'a set))}"
   and less_pos: "(x < y) = (pos x < pos y)"
diff -r 9465651c0db7 -r a8a9f4d79196 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 12:22:59 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Apr 19 14:17:41 2011 +0200
@@ -176,7 +176,7 @@
 
     val (((def1, def2), def3), lthy) = thy |>
 
-      Class.instantiation ([tyname'], [], @{sort enum}) |>
+      Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
 
       define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
         (p,
@@ -266,7 +266,7 @@
   in
     lthy' |>
     Local_Theory.note
-      ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
+      ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>>
     Local_Theory.note
       ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
     Local_Theory.note