src/HOL/Bali/Type.thy
changeset 35067 af4c18c30593
parent 32960 69916a850301
child 35069 09154b995ed8
--- a/src/HOL/Bali/Type.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Type.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -36,17 +36,11 @@
   "ref_ty"  <= (type) "Type.ref_ty"
   "ty"      <= (type) "Type.ty"
 
-syntax
-         NT     :: "       \<spacespace> ty"
-         Iface  :: "qtname  \<Rightarrow> ty"
-         Class  :: "qtname  \<Rightarrow> ty"
-         Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
-
-translations
-        "NT"      == "RefT   NullT"
-        "Iface I" == "RefT (IfaceT I)"
-        "Class C" == "RefT (ClassT C)"
-        "T.[]"    == "RefT (ArrayT T)"
+abbreviation "NT == RefT NullT"
+abbreviation "Iface I == RefT (IfaceT I)"
+abbreviation "Class C == RefT (ClassT C)"
+abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
+  where "T.[] == RefT (ArrayT T)"
 
 constdefs
   the_Class :: "ty \<Rightarrow> qtname"