# HG changeset patch
# User clasohm
# Date 805118244 -7200
# Node ID 9b2efb601898a6a5944875654ad7fa820d95a846
# Parent  7678408f97514baaa4ed34509ae1765bb8f26c51
moved mixfix syntax to Syntax/mixfix.ML

diff -r 7678408f9751 -r 9b2efb601898 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jul 05 20:14:22 1995 +0200
+++ b/src/Pure/sign.ML	Fri Jul 07 13:57:24 1995 +0200
@@ -544,25 +544,11 @@
   |> add_name "ProtoPure";
 
 val pure = proto_pure
-  |> add_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))]
+  |> add_syntax Syntax.pure_appl_syntax
   |> add_name "Pure";
 
 val cpure = proto_pure
-  |> add_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))]
+  |> add_syntax Syntax.pure_applC_syntax
   |> add_name "CPure";
 
 end;