# HG changeset patch
# User wenzelm
# Date 1187021424 -7200
# Node ID 9d0bb01f6634365c652fe5d2f7cfdd6ebf98e1b9
# Parent  3a915c75f7b66821a771555571cae5df9265b5a5
moved appl syntax to PureThy;
structure Lexicon: not hidden;

diff -r 3a915c75f7b6 -r 9d0bb01f6634 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Aug 13 18:10:24 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Aug 13 18:10:24 2007 +0200
@@ -68,8 +68,6 @@
   val merge_syntaxes: syntax -> syntax -> syntax
   val basic_syn: syntax
   val basic_nonterms: string list
-  val appl_syntax: (string * string * mixfix) list
-  val applC_syntax: (string * string * mixfix) list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
@@ -320,16 +318,6 @@
     SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
     "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]);
 
-val appl_syntax =
- [("_appl", "[('b => 'a), args] => logic", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
-  ("_appl", "[('b => 'a), args] => aprop", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
-
-val applC_syntax =
- [("",       "'a => cargs",                  Mixfix.Delimfix "_"),
-  ("_cargs", "['a, cargs] => cargs",         Mixfix.Mixfix ("_/ _", [1000, 1000], 1000)),
-  ("_applC", "[('b => 'a), cargs] => logic", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999)),
-  ("_applC", "[('b => 'a), cargs] => aprop", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999))];
-
 
 
 (** print syntax **)
@@ -564,7 +552,6 @@
 open BasicSyntax;
 
 structure Hidden = struct end;
-structure Lexicon = Hidden;
 structure Ast = Hidden;
 structure SynExt = Hidden;
 structure Parser = Hidden;