diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/CodeEmbed.thy
--- a/src/HOL/ex/CodeEmbed.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -22,9 +22,10 @@
   | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
 
 abbreviation
-  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
   "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
-  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
+abbreviation
+  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
   "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
 
 datatype "term" =
@@ -33,7 +34,7 @@
   | App   "term" "term" (infixl "\<bullet>" 110)
 
 abbreviation
-  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110)
+  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110) where
   "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"