# 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;