moved appl syntax to PureThy;
authorwenzelm
Mon Aug 13 18:10:24 2007 +0200 (2007-08-13)
changeset 242479d0bb01f6634
parent 24246 3a915c75f7b6
child 24248 d276e4b53d6b
moved appl syntax to PureThy;
structure Lexicon: not hidden;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Aug 13 18:10:24 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Aug 13 18:10:24 2007 +0200
     1.3 @@ -68,8 +68,6 @@
     1.4    val merge_syntaxes: syntax -> syntax -> syntax
     1.5    val basic_syn: syntax
     1.6    val basic_nonterms: string list
     1.7 -  val appl_syntax: (string * string * mixfix) list
     1.8 -  val applC_syntax: (string * string * mixfix) list
     1.9    val print_gram: syntax -> unit
    1.10    val print_trans: syntax -> unit
    1.11    val print_syntax: syntax -> unit
    1.12 @@ -320,16 +318,6 @@
    1.13      SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
    1.14      "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]);
    1.15  
    1.16 -val appl_syntax =
    1.17 - [("_appl", "[('b => 'a), args] => logic", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
    1.18 -  ("_appl", "[('b => 'a), args] => aprop", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    1.19 -
    1.20 -val applC_syntax =
    1.21 - [("",       "'a => cargs",                  Mixfix.Delimfix "_"),
    1.22 -  ("_cargs", "['a, cargs] => cargs",         Mixfix.Mixfix ("_/ _", [1000, 1000], 1000)),
    1.23 -  ("_applC", "[('b => 'a), cargs] => logic", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999)),
    1.24 -  ("_applC", "[('b => 'a), cargs] => aprop", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999))];
    1.25 -
    1.26  
    1.27  
    1.28  (** print syntax **)
    1.29 @@ -564,7 +552,6 @@
    1.30  open BasicSyntax;
    1.31  
    1.32  structure Hidden = struct end;
    1.33 -structure Lexicon = Hidden;
    1.34  structure Ast = Hidden;
    1.35  structure SynExt = Hidden;
    1.36  structure Parser = Hidden;