src/Pure/sign.ML

                                                     [max_pri, 0], max_pri))]
   |> add_name "Pure";
 
 val cpure = proto_pure
   |> add_syntax
-   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("(1_ (1_))",
+   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("_/ _",
                                                     [max_pri-1, max_pri],
                                                     max_pri-1)),
-    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("(1_ (1_))",
+    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("_/ _",
                                                     [max_pri-1, max_pri],
                                                     max_pri-1))]
   |> add_name "CPure";
 
 end;