--- a/src/HOL/Bali/Type.thy Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Type.thy Mon Jul 26 17:41:26 2010 +0200
@@ -36,8 +36,9 @@
abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90)
where "T.[] == RefT (ArrayT T)"
-definition the_Class :: "ty \<Rightarrow> qtname" where
- "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
+definition
+ the_Class :: "ty \<Rightarrow> qtname"
+ where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)