diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
-    ID:         $Id$
     Author:     Gerwin Klein
 *)
 
@@ -13,9 +12,9 @@
 datatype 'a type_error = TypeError | Normal 'a
 
 
-syntax "fifth" :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
-translations
-  "fifth x" == "fst(snd(snd(snd(snd x))))"
+abbreviation
+  fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
+  where "fifth x == fst(snd(snd(snd(snd x))))"
 
 
 consts isAddr :: "val \<Rightarrow> bool"