# HG changeset patch
# User clasohm
# Date 796565250 -7200
# Node ID c978bb4e9a554644cdd99c95259a06794fae8aa1
# Parent  2e50c5124ca31fd0905474634efc61cfdcd4d24b
changed pretty printing of applC

diff -r 2e50c5124ca3 -r c978bb4e9a55 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Mar 30 14:01:35 1995 +0200
+++ b/src/Pure/sign.ML	Thu Mar 30 14:07:30 1995 +0200
@@ -554,10 +554,10 @@
 
 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";