src/HOL/Bali/Value.thy
changeset 35431 8758fe1fc9f8
parent 35069 09154b995ed8
child 37956 ee939247b2fb
--- 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"