src/Pure/sign.ML
changeset 986 c978bb4e9a55
parent 963 7a78fda77104
child 1159 998a5c3451bf
     1.1 --- a/src/Pure/sign.ML	Thu Mar 30 14:01:35 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Mar 30 14:07:30 1995 +0200
     1.3 @@ -554,10 +554,10 @@
     1.4  
     1.5  val cpure = proto_pure
     1.6    |> add_syntax
     1.7 -   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("(1_ (1_))",
     1.8 +   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("_/ _",
     1.9                                                      [max_pri-1, max_pri],
    1.10                                                      max_pri-1)),
    1.11 -    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("(1_ (1_))",
    1.12 +    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("_/ _",
    1.13                                                      [max_pri-1, max_pri],
    1.14                                                      max_pri-1))]
    1.15    |> add_name "CPure";