diff -r 6ce9177d6b38 -r cc7a0b9f938c src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Feb 11 00:45:02 2010 +0100
@@ -262,10 +262,8 @@
 done
 
 
-syntax
-  mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c"
-translations
-  "mtd_mb" => "Fun.comp snd snd"
+abbreviation (input)
+  "mtd_mb == snd o snd"
 
 lemma map_of_map_fst: "\<lbrakk> inj f;
   \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>