# HG changeset patch
# User wenzelm
# Date 1267572782 -3600
# Node ID 8758fe1fc9f8b7b1e5cdd13237b77f0ea37c7ab7
# Parent  df2862dc23a828d6d5773c2f93b3ffd7d044815a
cleanup type translations;

diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -58,10 +58,9 @@
   "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
 
   --{* relation on result values, state and auxiliary variables *}
-types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 translations
-      "res"    <= (type) "AxSem.res"
-      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
+  (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 
 definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
  "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Basis.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -213,11 +213,6 @@
 *}
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
 
-translations
-  "option"<= (type) "Option.option"
-  "list"  <= (type) "List.list"
-  "sum3"  <= (type) "Basis.sum3"
-
 
 section "quantifiers for option type"
 
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -149,24 +149,24 @@
         access :: acc_modi
 
 translations
-  "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
-  "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
+  (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
+  (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
 
 subsection {* Member (field or method)*}
 record  member = decl +
          static :: stat_modi
 
 translations
-  "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
-  "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
+  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
+  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
 
 subsection {* Field *}
 
 record field = member +
         type :: ty
 translations
-  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
-  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
+  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
+  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
 
 types     
         fdecl           (* field declaration, cf. 8.3 *)
@@ -174,7 +174,7 @@
 
 
 translations
-  "fdecl" <= (type) "vname \<times> field"
+  (type) "fdecl" <= (type) "vname \<times> field"
 
 subsection  {* Method *}
 
@@ -193,17 +193,17 @@
 
 
 translations
-  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
+  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
                       pars::vname list, resT::ty\<rparr>"
-  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
+  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
                       pars::vname list, resT::ty,\<dots>::'a\<rparr>"
-  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
-  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
-  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
+  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
+  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
+  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
                       pars::vname list, resT::ty,mbody::mbody\<rparr>"
-  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
+  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
                       pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
-  "mdecl" <= (type) "sig \<times> methd"
+  (type) "mdecl" <= (type) "sig \<times> methd"
 
 
 definition mhead :: "methd \<Rightarrow> mhead" where
@@ -306,13 +306,13 @@
         = "qtname \<times> iface"
 
 translations
-  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
-  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
-  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
+  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
+  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
                       isuperIfs::qtname list\<rparr>"
-  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
                       isuperIfs::qtname list,\<dots>::'a\<rparr>"
-  "idecl" <= (type) "qtname \<times> iface"
+  (type) "idecl" <= (type) "qtname \<times> iface"
 
 definition ibody :: "iface \<Rightarrow> ibody" where
   "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
@@ -337,17 +337,17 @@
         = "qtname \<times> class"
 
 translations
-  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
                       methods::mdecl list,init::stmt\<rparr>"
-  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
                       methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
-  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
                       methods::mdecl list,init::stmt,
                       super::qtname,superIfs::qtname list\<rparr>"
-  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
                       methods::mdecl list,init::stmt,
                       super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
-  "cdecl" <= (type) "qtname \<times> class"
+  (type) "cdecl" <= (type) "qtname \<times> class"
 
 definition cbody :: "class \<Rightarrow> cbody" where
   "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
@@ -404,8 +404,8 @@
         "classes"::"cdecl list"
 
 translations
-     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
-     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
+     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
+     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
 
 abbreviation
   iface :: "prog  \<Rightarrow> (qtname, iface) table"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -1377,7 +1377,7 @@
   fspec = "vname \<times> qtname"
 
 translations 
-  "fspec" <= (type) "vname \<times> qtname" 
+  (type) "fspec" <= (type) "vname \<times> qtname" 
 
 definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
 "imethds G I 
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Eval.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -99,8 +99,8 @@
 types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
       vals  =        "(val, vvar, val list) sum3"
 translations
-     "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
-     "vals" <= (type)"(val, vvar, val list) sum3" 
+  (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+  (type) "vals" <= (type) "(val, vvar, val list) sum3" 
 
 text {* To avoid redundancy and to reduce the number of rules, there is only 
  one evaluation rule for each syntactic term. This is also true for variables
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Name.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -78,11 +78,7 @@
   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
 
 translations
-  "mname"  <= "Name.mname"
-  "xname"  <= "Name.xname"
-  "tname"  <= "Name.tname"
-  "ename"  <= "Name.ename"
-  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+  (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
 
 
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/State.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -33,10 +33,10 @@
           "values" :: "(vn, val) table"      
 
 translations 
-  "fspec" <= (type) "vname \<times> qtname" 
-  "vn"    <= (type) "fspec + int"
-  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
-  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
+  (type) "fspec" <= (type) "vname \<times> qtname" 
+  (type) "vn"    <= (type) "fspec + int"
+  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
+  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
 
 definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
  "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
@@ -134,7 +134,7 @@
 translations
   "Heap" => "CONST Inl"
   "Stat" => "CONST Inr"
-  "oref" <= (type) "loc + qtname"
+  (type) "oref" <= (type) "loc + qtname"
 
 definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
  "fields_table G C P 
@@ -213,9 +213,9 @@
         = "(lname, val) table" *) (* defined in Value.thy local variables *)
 
 translations
- "globs"  <= (type) "(oref , obj) table"
- "heap"   <= (type) "(loc  , obj) table"
-(*  "locals" <= (type) "(lname, val) table" *)
+ (type) "globs"  <= (type) "(oref , obj) table"
+ (type) "heap"   <= (type) "(loc  , obj) table"
+(*  (type) "locals" <= (type) "(lname, val) table" *)
 
 datatype st = (* pure state, i.e. contents of all variables *)
          st globs locals
@@ -567,10 +567,8 @@
   state = "abopt \<times> st"          --{* state including abruption information *}
 
 translations
-  "abopt"       <= (type) "State.abrupt option"
-  "abopt"       <= (type) "abrupt option"
-  "state"      <= (type) "abopt \<times> State.st"
-  "state"      <= (type) "abopt \<times> st"
+  (type) "abopt" <= (type) "abrupt option"
+  (type) "state" <= (type) "abopt \<times> st"
 
 abbreviation
   Norm :: "st \<Rightarrow> state"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Table.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -42,8 +42,7 @@
   where "table_of \<equiv> map_of"
 
 translations
-  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
-  (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
+  (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
 
 (* ### To map *)
 lemma map_add_find_left[simp]:
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Term.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -88,7 +88,7 @@
 statement *}
 
 translations
- "locals" <= (type) "(lname, val) table"
+ (type) "locals" <= (type) "(lname, val) table"
 
 datatype inv_mode                  --{* invocation mode for method calls *}
         = Static                   --{* static *}
@@ -100,8 +100,8 @@
           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*} 
@@ -237,11 +237,8 @@
  
 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)"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Type.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -30,11 +30,6 @@
         = PrimT prim_ty --{* primitive type *}
         | RefT  ref_ty  --{* reference type *}
 
-translations
-  "prim_ty" <= (type) "Type.prim_ty"
-  "ref_ty"  <= (type) "Type.ref_ty"
-  "ty"      <= (type) "Type.ty"
-
 abbreviation "NT == RefT NullT"
 abbreviation "Iface I == RefT (IfaceT I)"
 abbreviation "Class C == RefT (ClassT C)"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Value.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -17,9 +17,6 @@
         | Addr loc      --{* addresses, i.e. locations of objects *}
 
 
-translations "val" <= (type) "Term.val"
-             "loc" <= (type) "Term.loc"
-
 consts   the_Bool   :: "val \<Rightarrow> bool"  
 primrec "the_Bool (Bool b) = b"
 consts   the_Intg   :: "val \<Rightarrow> int"
diff -r df2862dc23a8 -r 8758fe1fc9f8 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
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -18,7 +18,7 @@
 
 types 'a assn = "'a => state => bool"
 translations
-  "a assn"   <= (type)"a => state => bool"
+  (type) "'a assn" <= (type) "'a => state => bool"
 
 definition
   state_not_singleton :: bool where
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -32,7 +32,7 @@
 
 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
 
-translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
+translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
 
 typed_print_translation {*
 let
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -23,12 +23,12 @@
 
 
 translations
-  "fdecl"   <= (type) "vname \<times> ty"
-  "sig"     <= (type) "mname \<times> ty list"
-  "mdecl c" <= (type) "sig \<times> ty \<times> c"
-  "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
-  "cdecl c" <= (type) "cname \<times> (c class)"
-  "prog  c" <= (type) "(c cdecl) list"
+  (type) "fdecl" <= (type) "vname \<times> ty"
+  (type) "sig" <= (type) "mname \<times> ty list"
+  (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
+  (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
+  (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
+  (type) "'c prog" <= (type) "('c cdecl) list"
 
 
 definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -13,10 +13,10 @@
       triple = "assn \<times> stmt \<times>  assn"
      etriple = "assn \<times> expr \<times> vassn"
 translations
-  "assn"   \<leftharpoondown> (type)"state => bool"
- "vassn"   \<leftharpoondown> (type)"val => assn"
-  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
- "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
+  (type) "assn" \<leftharpoondown> (type) "state => bool"
+  (type) "vassn" \<leftharpoondown> (type) "val => assn"
+  (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
+  (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
 
 
 subsection "Hoare Logic Rules"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -38,11 +38,11 @@
         = "cdecl list"
 
 translations
-  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
-  "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
-  "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
-  "cdecl" \<leftharpoondown> (type)"cname \<times> class"
-  "prog " \<leftharpoondown> (type)"cdecl list"
+  (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
+  (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
+  (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
+  (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
+  (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
 consts
 
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/State.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -23,9 +23,8 @@
         obj = "cname \<times> fields"
 
 translations
-
-  "fields" \<leftharpoondown> (type)"fname => val option"
-  "obj"    \<leftharpoondown> (type)"cname \<times> fields"
+  (type) "fields" \<leftharpoondown> (type) "fname => val option"
+  (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
 
 definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
  "init_vars m == Option.map (\<lambda>T. Null) o m"
@@ -40,10 +39,9 @@
           locals :: locals
 
 translations
-
-  "heap"   \<leftharpoondown> (type)"loc   => obj option"
-  "locals" \<leftharpoondown> (type)"vname => val option"
-  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
+  (type) "heap" \<leftharpoondown> (type) "loc => obj option"
+  (type) "locals" \<leftharpoondown> (type) "vname => val option"
+  (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
 
 definition del_locs :: "state => state" where
  "del_locs s \<equiv> s (| locals := empty |)"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/One.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -10,7 +10,7 @@
 
 types one = "unit lift"
 translations
-  "one" <= (type) "unit lift" 
+  (type) "one" <= (type) "unit lift" 
 
 definition
   ONE :: "one"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -49,7 +49,7 @@
 text "A TypeRep is an algebraic deflation over the universe of values."
 
 types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
 
 definition
   Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -59,7 +59,7 @@
       (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
 
 syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
 
 lemma cast_REP:
   "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Tr.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -14,7 +14,7 @@
   tr = "bool lift"
 
 translations
-  "tr" <= (type) "bool lift"
+  (type) "tr" <= (type) "bool lift"
 
 definition
   TT :: "tr" where