src/HOL/Bali/Term.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/Term.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/Term.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  statement *}
     1.5  
     1.6  translations
     1.7 - "locals" <= (type) "(lname, val) table"
     1.8 + (type) "locals" <= (type) "(lname, val) table"
     1.9  
    1.10  datatype inv_mode                  --{* invocation mode for method calls *}
    1.11          = Static                   --{* static *}
    1.12 @@ -100,8 +100,8 @@
    1.13            parTs::"ty list"        
    1.14  
    1.15  translations
    1.16 -  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    1.17 -  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    1.18 +  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    1.19 +  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    1.20  
    1.21  --{* function codes for unary operations *}
    1.22  datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
    1.23 @@ -237,11 +237,8 @@
    1.24   
    1.25  types "term" = "(expr+stmt,var,expr list) sum3"
    1.26  translations
    1.27 -  "sig"   <= (type) "mname \<times> ty list"
    1.28 -  "var"   <= (type) "Term.var"
    1.29 -  "expr"  <= (type) "Term.expr"
    1.30 -  "stmt"  <= (type) "Term.stmt"
    1.31 -  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    1.32 +  (type) "sig"   <= (type) "mname \<times> ty list"
    1.33 +  (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    1.34  
    1.35  abbreviation this :: expr
    1.36    where "this == Acc (LVar This)"