| changeset 42 | d981488bda7b |
| parent 18 | c9ec452ff08f |
| child 116 | fdc1c3424247 |
--- 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);