removed obsolete appl_syntax, applC_syntax;
authorwenzelm
Thu Mar 27 15:32:19 2008 +0100 (2008-03-27)
changeset 26436dfd6947ab5c2
parent 26435 bdce320cd426
child 26437 5906619c8c6b
removed obsolete appl_syntax, applC_syntax;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Thu Mar 27 15:32:15 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Mar 27 15:32:19 2008 +0100
     1.3 @@ -72,8 +72,6 @@
     1.4      theory -> thm list * theory
     1.5    val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
     1.6      theory -> thm list * theory
     1.7 -  val appl_syntax: (string * typ * mixfix) list
     1.8 -  val applC_syntax: (string * typ * mixfix) list
     1.9  end;
    1.10  
    1.11  structure PureThy: PURE_THY =
    1.12 @@ -427,16 +425,6 @@
    1.13  val term = SimpleSyntax.read_term;
    1.14  val prop = SimpleSyntax.read_prop;
    1.15  
    1.16 -val appl_syntax =
    1.17 - [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
    1.18 -  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    1.19 -
    1.20 -val applC_syntax =
    1.21 - [("",       typ "'a => cargs",                  Delimfix "_"),
    1.22 -  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
    1.23 -  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
    1.24 -  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
    1.25 -
    1.26  val _ = Context.>>
    1.27    (Sign.add_types
    1.28     [("fun", 2, NoSyn),
    1.29 @@ -445,44 +433,45 @@
    1.30      ("dummy", 0, NoSyn)]
    1.31    #> Sign.add_nonterminals Syntax.basic_nonterms
    1.32    #> Sign.add_syntax_i
    1.33 -   [("_lambda",     typ "pttrns => 'a => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
    1.34 -    ("_abs",        typ "'a",                        NoSyn),
    1.35 -    ("",            typ "'a => args",                Delimfix "_"),
    1.36 -    ("_args",       typ "'a => args => args",        Delimfix "_,/ _"),
    1.37 -    ("",            typ "id => idt",                 Delimfix "_"),
    1.38 -    ("_idtdummy",   typ "idt",                       Delimfix "'_"),
    1.39 -    ("_idtyp",      typ "id => type => idt",         Mixfix ("_::_", [], 0)),
    1.40 -    ("_idtypdummy", typ "type => idt",               Mixfix ("'_()::_", [], 0)),
    1.41 -    ("",            typ "idt => idt",                Delimfix "'(_')"),
    1.42 -    ("",            typ "idt => idts",               Delimfix "_"),
    1.43 -    ("_idts",       typ "idt => idts => idts",       Mixfix ("_/ _", [1, 0], 0)),
    1.44 -    ("",            typ "idt => pttrn",              Delimfix "_"),
    1.45 -    ("",            typ "pttrn => pttrns",           Delimfix "_"),
    1.46 -    ("_pttrns",     typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
    1.47 -    ("",            typ "id => aprop",               Delimfix "_"),
    1.48 -    ("",            typ "longid => aprop",           Delimfix "_"),
    1.49 -    ("",            typ "var => aprop",              Delimfix "_"),
    1.50 -    ("_DDDOT",      typ "aprop",                     Delimfix "..."),
    1.51 -    ("_aprop",      typ "aprop => prop",             Delimfix "PROP _"),
    1.52 -    ("_asm",        typ "prop => asms",              Delimfix "_"),
    1.53 -    ("_asms",       typ "prop => asms => asms",      Delimfix "_;/ _"),
    1.54 -    ("_bigimpl",    typ "asms => prop => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    1.55 -    ("_ofclass",    typ "type => logic => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.56 -    ("_mk_ofclass", typ "dummy",                     NoSyn),
    1.57 -    ("_TYPE",       typ "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
    1.58 -    ("",            typ "id => logic",               Delimfix "_"),
    1.59 -    ("",            typ "longid => logic",           Delimfix "_"),
    1.60 -    ("",            typ "var => logic",              Delimfix "_"),
    1.61 -    ("_DDDOT",      typ "logic",                     Delimfix "..."),
    1.62 -    ("_constify",   typ "num => num_const",          Delimfix "_"),
    1.63 -    ("_indexnum",   typ "num_const => index",        Delimfix "\\<^sub>_"),
    1.64 -    ("_index",      typ "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.65 -    ("_indexdefault", typ "index",                   Delimfix ""),
    1.66 -    ("_indexvar",   typ "index",                     Delimfix "'\\<index>"),
    1.67 -    ("_struct",     typ "index => logic",            Mixfix ("\\<struct>_", [1000], 1000)),
    1.68 -    ("==>",         typ "prop => prop => prop",      Delimfix "op ==>"),
    1.69 -    (Term.dummy_patternN, typ "aprop",               Delimfix "'_")]
    1.70 -  #> Sign.add_syntax_i appl_syntax
    1.71 +   [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
    1.72 +    ("_abs",        typ "'a",                          NoSyn),
    1.73 +    ("",            typ "'a => args",                  Delimfix "_"),
    1.74 +    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
    1.75 +    ("",            typ "id => idt",                   Delimfix "_"),
    1.76 +    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
    1.77 +    ("_idtyp",      typ "id => type => idt",           Mixfix ("_::_", [], 0)),
    1.78 +    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
    1.79 +    ("",            typ "idt => idt",                  Delimfix "'(_')"),
    1.80 +    ("",            typ "idt => idts",                 Delimfix "_"),
    1.81 +    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
    1.82 +    ("",            typ "idt => pttrn",                Delimfix "_"),
    1.83 +    ("",            typ "pttrn => pttrns",             Delimfix "_"),
    1.84 +    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
    1.85 +    ("",            typ "id => aprop",                 Delimfix "_"),
    1.86 +    ("",            typ "longid => aprop",             Delimfix "_"),
    1.87 +    ("",            typ "var => aprop",                Delimfix "_"),
    1.88 +    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
    1.89 +    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
    1.90 +    ("_asm",        typ "prop => asms",                Delimfix "_"),
    1.91 +    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
    1.92 +    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    1.93 +    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.94 +    ("_mk_ofclass", typ "dummy",                       NoSyn),
    1.95 +    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
    1.96 +    ("",            typ "id => logic",                 Delimfix "_"),
    1.97 +    ("",            typ "longid => logic",             Delimfix "_"),
    1.98 +    ("",            typ "var => logic",                Delimfix "_"),
    1.99 +    ("_DDDOT",      typ "logic",                       Delimfix "..."),
   1.100 +    ("_constify",   typ "num => num_const",            Delimfix "_"),
   1.101 +    ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
   1.102 +    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
   1.103 +    ("_indexdefault", typ "index",                     Delimfix ""),
   1.104 +    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
   1.105 +    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
   1.106 +    ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
   1.107 +    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
   1.108 +    ("_appl",       typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
   1.109 +    ("_appl",       typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]
   1.110    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   1.111     [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   1.112      ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),