src/HOL/Bali/Term.thy

 we save the local variables of the caller in the term Callee to restore them 
 after method return. Also an exception must be restored after the finally
 statement *}
 
 translations
- "locals" <= (type) "(lname, val) table"
+ (type) "locals" <= (type) "(lname, val) table"
 
 datatype inv_mode                  --{* invocation mode for method calls *}
         = Static                   --{* static *}
         | SuperM                   --{* super  *}
         | IntVir                   --{* interface or virtual *}

 record  sig =              --{* signature of a method, cf. 8.4.2  *}
           name ::"mname"   --{* acutally belongs to Decl.thy *}
           parTs::"ty list"        
 
 translations
-  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
-  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
+  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
+  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
 
 --{* function codes for unary operations *}
 datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
                | UMinus   -- {*{\tt -} unary minus*}
                | UBitNot  -- {*{\tt ~} bitwise NOT*}

 intermediate steps of class-initialisation.
 *}
  
 types "term" = "(expr+stmt,var,expr list) sum3"
 translations
-  "sig"   <= (type) "mname \<times> ty list"
-  "var"   <= (type) "Term.var"
-  "expr"  <= (type) "Term.expr"
-  "stmt"  <= (type) "Term.stmt"
-  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
+  (type) "sig"   <= (type) "mname \<times> ty list"
+  (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
 
 abbreviation this :: expr
   where "this == Acc (LVar This)"
 
 abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")