src/HOL/Bali/Type.thy

--- a/src/HOL/Bali/Type.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Bali/Type.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -41,8 +41,7 @@
 abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
   where "T.[] == RefT (ArrayT T)"
 
-constdefs
-  the_Class :: "ty \<Rightarrow> qtname"
+definition the_Class :: "ty \<Rightarrow> qtname" where
  "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
  
 lemma the_Class_eq [simp]: "the_Class (Class C)= C"