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 \ bool" primrec "the_Bool (Bool b) = b" consts the_Intg :: "val \ int"