diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Sum_Type.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -40,7 +40,7 @@
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
 
-  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
+  sum_def       "A <+> B == (Inl`A) Un (Inr`B)"
 
   (*for selecting out the components of a mutually recursive definition*)
   Part_def      "Part A h == A Int {x. ? z. x = h(z)}"