src/HOL/Bali/WellType.thy

--- a/src/HOL/Bali/WellType.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/WellType.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -37,10 +37,10 @@
          lcl:: "lenv"    --{* local environment *}     
   
 translations
-  "lenv" <= (type) "(lname, ty) table"
-  "lenv" <= (type) "lname \<Rightarrow> ty option"
-  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
-  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
+  (type) "lenv" <= (type) "(lname, ty) table"
+  (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
+  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
+  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
 
 
 abbreviation
@@ -238,9 +238,9 @@
 
 section "Typing for terms"
 
-types tys  =        "ty + ty list"
+types tys  = "ty + ty list"
 translations
-  "tys"   <= (type) "ty + ty list"
+  (type) "tys" <= (type) "ty + ty list"
 
 
 inductive