diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellType.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -43,11 +43,9 @@
   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
 
 
-
-syntax
+abbreviation
   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
-translations 
-  "pkg e" == "pid (cls e)"
+  where "pkg e == pid (cls e)"
 
 section "Static overloading: maximally specific methods "
 
@@ -426,29 +424,33 @@
                                          E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
 
 
-syntax (* for purely static typing *)
-  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
-  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
-  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
-  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
-  "_ty_exprs":: "env \<Rightarrow> [expr list,
-                     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+(* for purely static typing *)
+abbreviation
+  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
+
+abbreviation
+  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
+  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
+
+abbreviation
+  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+  where "E|-e:-T == E|-In1l e :: Inl T"
 
-syntax (xsymbols)
-  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
-  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
-  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
-  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
-  "_ty_exprs" :: "env \<Rightarrow> [expr list,
-                    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+abbreviation
+  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+  where "E|-e:=T == E|-In2 e :: Inl T"
 
-translations
-        "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
-        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
-        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
-        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
-        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
+abbreviation
+  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+  where "E|-e:#T == E|-In3 e :: Inr T"
 
+notation (xsymbols)
+  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
+  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
+  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
+  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
+  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
 
 declare not_None_eq [simp del] 
 declare split_if [split del] split_if_asm [split del]