--- a/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 14:04:58 2011 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 14:20:13 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)"
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Apr 19 14:04:58 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Apr 19 14:20:13 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