# HG changeset patch
# User wenzelm
# Date 1206628339 -3600
# Node ID dfd6947ab5c29131078ef5ab0ff3eaefc620adae
# Parent  bdce320cd426299479af72100d96726b83570970
removed obsolete appl_syntax, applC_syntax;

diff -r bdce320cd426 -r dfd6947ab5c2 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Mar 27 15:32:15 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Mar 27 15:32:19 2008 +0100
@@ -72,8 +72,6 @@
     theory -> thm list * theory
   val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
     theory -> thm list * theory
-  val appl_syntax: (string * typ * mixfix) list
-  val applC_syntax: (string * typ * mixfix) list
 end;
 
 structure PureThy: PURE_THY =
@@ -427,16 +425,6 @@
 val term = SimpleSyntax.read_term;
 val prop = SimpleSyntax.read_prop;
 
-val appl_syntax =
- [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
-  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
-
-val applC_syntax =
- [("",       typ "'a => cargs",                  Delimfix "_"),
-  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
-  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
-  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
-
 val _ = Context.>>
   (Sign.add_types
    [("fun", 2, NoSyn),
@@ -445,44 +433,45 @@
     ("dummy", 0, NoSyn)]
   #> Sign.add_nonterminals Syntax.basic_nonterms
   #> Sign.add_syntax_i
-   [("_lambda",     typ "pttrns => 'a => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
-    ("_abs",        typ "'a",                        NoSyn),
-    ("",            typ "'a => args",                Delimfix "_"),
-    ("_args",       typ "'a => args => args",        Delimfix "_,/ _"),
-    ("",            typ "id => idt",                 Delimfix "_"),
-    ("_idtdummy",   typ "idt",                       Delimfix "'_"),
-    ("_idtyp",      typ "id => type => idt",         Mixfix ("_::_", [], 0)),
-    ("_idtypdummy", typ "type => idt",               Mixfix ("'_()::_", [], 0)),
-    ("",            typ "idt => idt",                Delimfix "'(_')"),
-    ("",            typ "idt => idts",               Delimfix "_"),
-    ("_idts",       typ "idt => idts => idts",       Mixfix ("_/ _", [1, 0], 0)),
-    ("",            typ "idt => pttrn",              Delimfix "_"),
-    ("",            typ "pttrn => pttrns",           Delimfix "_"),
-    ("_pttrns",     typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
-    ("",            typ "id => aprop",               Delimfix "_"),
-    ("",            typ "longid => aprop",           Delimfix "_"),
-    ("",            typ "var => aprop",              Delimfix "_"),
-    ("_DDDOT",      typ "aprop",                     Delimfix "..."),
-    ("_aprop",      typ "aprop => prop",             Delimfix "PROP _"),
-    ("_asm",        typ "prop => asms",              Delimfix "_"),
-    ("_asms",       typ "prop => asms => asms",      Delimfix "_;/ _"),
-    ("_bigimpl",    typ "asms => prop => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
-    ("_ofclass",    typ "type => logic => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
-    ("_mk_ofclass", typ "dummy",                     NoSyn),
-    ("_TYPE",       typ "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
-    ("",            typ "id => logic",               Delimfix "_"),
-    ("",            typ "longid => logic",           Delimfix "_"),
-    ("",            typ "var => logic",              Delimfix "_"),
-    ("_DDDOT",      typ "logic",                     Delimfix "..."),
-    ("_constify",   typ "num => num_const",          Delimfix "_"),
-    ("_indexnum",   typ "num_const => index",        Delimfix "\\<^sub>_"),
-    ("_index",      typ "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
-    ("_indexdefault", typ "index",                   Delimfix ""),
-    ("_indexvar",   typ "index",                     Delimfix "'\\<index>"),
-    ("_struct",     typ "index => logic",            Mixfix ("\\<struct>_", [1000], 1000)),
-    ("==>",         typ "prop => prop => prop",      Delimfix "op ==>"),
-    (Term.dummy_patternN, typ "aprop",               Delimfix "'_")]
-  #> Sign.add_syntax_i appl_syntax
+   [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
+    ("_abs",        typ "'a",                          NoSyn),
+    ("",            typ "'a => args",                  Delimfix "_"),
+    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
+    ("",            typ "id => idt",                   Delimfix "_"),
+    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
+    ("_idtyp",      typ "id => type => idt",           Mixfix ("_::_", [], 0)),
+    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
+    ("",            typ "idt => idt",                  Delimfix "'(_')"),
+    ("",            typ "idt => idts",                 Delimfix "_"),
+    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
+    ("",            typ "idt => pttrn",                Delimfix "_"),
+    ("",            typ "pttrn => pttrns",             Delimfix "_"),
+    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
+    ("",            typ "id => aprop",                 Delimfix "_"),
+    ("",            typ "longid => aprop",             Delimfix "_"),
+    ("",            typ "var => aprop",                Delimfix "_"),
+    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
+    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
+    ("_asm",        typ "prop => asms",                Delimfix "_"),
+    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
+    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
+    ("_mk_ofclass", typ "dummy",                       NoSyn),
+    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
+    ("",            typ "id => logic",                 Delimfix "_"),
+    ("",            typ "longid => logic",             Delimfix "_"),
+    ("",            typ "var => logic",                Delimfix "_"),
+    ("_DDDOT",      typ "logic",                       Delimfix "..."),
+    ("_constify",   typ "num => num_const",            Delimfix "_"),
+    ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
+    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
+    ("_indexdefault", typ "index",                     Delimfix ""),
+    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
+    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
+    ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
+    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
+    ("_appl",       typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
+    ("_appl",       typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]
   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
     ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),