author | wenzelm |
Mon, 15 Nov 1993 10:30:37 +0100 | |
changeset 117 | 6b26ccac50fc |
parent 116 | fdc1c3424247 |
child 118 | 96d2c0fc2cd5 |
--- a/src/Pure/Syntax/extension.ML Sun Nov 14 15:14:30 1993 +0100 +++ b/src/Pure/Syntax/extension.ML Mon Nov 15 10:30:37 1993 +0100 @@ -233,7 +233,7 @@ let fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0); - fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri); + fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri); fun mkappl T = Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);