# HG changeset patch # User nipkow # Date 753020687 -3600 # Node ID 1e669b5a75f9684a1829c52f09cf6ff1c5a0a6a3 # Parent 009ae5c85ae917d13a71ec085f8bda5b3bcfbc38 changed formatting for application diff -r 009ae5c85ae9 -r 1e669b5a75f9 src/Pure/Syntax/sextension.ML --- a/src/Pure/Syntax/sextension.ML Thu Nov 11 13:21:59 1993 +0100 +++ b/src/Pure/Syntax/sextension.ML Thu Nov 11 13:24:47 1993 +0100 @@ -438,7 +438,7 @@ Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), Delimfix ("_", "id => aprop", ""), Delimfix ("_", "var => aprop", ""), - Mixfix ("_/(1'(_'))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), + Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), Delimfix ("PROP _", "aprop => prop", "_aprop"), Delimfix ("_", "prop => asms", ""), Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"),