# HG changeset patch
# User clasohm
# Date 805118263 -7200
# Node ID c4e90fb7f8fa3843605ace461ecc1dcafe913802
# Parent  9b2efb601898a6a5944875654ad7fa820d95a846
moved mixfix syntax from sign.ML

diff -r 9b2efb601898 -r c4e90fb7f8fa src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Jul 07 13:57:24 1995 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Jul 07 13:57:43 1995 +0200
@@ -24,6 +24,8 @@
   val const_name: string -> mixfix -> string
   val pure_types: (string * int * mixfix) list
   val pure_syntax: (string * string * mixfix) list
+  val pure_appl_syntax: (string * string * mixfix) list
+  val pure_applC_syntax: (string * string * mixfix) list
 end;
 
 signature MIXFIX =
@@ -164,4 +166,21 @@
   ("",          "id => logic",                    Delimfix "_"),
   ("",          "var => logic",                   Delimfix "_")]
 
+val pure_appl_syntax =
+ [("_appl",     "[('b => 'a), args] => logic",    Mixfix ("(1_/(1'(_')))",
+                                                    [max_pri, 0], max_pri)),
+  ("_appl",     "[('b => 'a), args] => aprop",    Mixfix ("(1_/(1'(_')))",
+                                                    [max_pri, 0], max_pri))];
+
+val pure_applC_syntax =
+ [("",           "'a => cargs",                   Delimfix "_"),
+  ("_cargs",     "['a, cargs] => cargs",          Mixfix ("_/ _",
+                                                   [max_pri, max_pri],
+                                                   max_pri)),
+  ("_applC",     "[('b => 'a), cargs] => logic",  Mixfix ("(1_/ _)",
+                                                   [max_pri, max_pri],
+                                                   max_pri-1)),
+  ("_applC",     "[('b => 'a), cargs] => aprop",  Mixfix ("(1_/ _)",
+                                                   [max_pri, max_pri],
+                                                   max_pri-1))];
 end;