diff -r 97aae241094b -r d981488bda7b src/Pure/Syntax/extension.ML
--- a/src/Pure/Syntax/extension.ML	Fri Oct 08 12:35:53 1993 +0100
+++ b/src/Pure/Syntax/extension.ML	Fri Oct 08 13:55:04 1993 +0100
@@ -236,7 +236,7 @@
     fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri);
 
     fun mkappl T =
-      Mfix ("_(1'(_'))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
+      Mfix ("_/(1'(_'))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
 
     fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);