type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);

--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 21:55:41 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 22:25:44 2011 +0200
@@ -640,10 +640,7 @@
 
 (* basic syntax *)
 
-val basic_syntax =
-  empty_syntax
-  |> update_syntax mode_default Type_Ext.type_ext
-  |> update_syntax mode_default Syn_Ext.pure_ext;
+val basic_syntax = update_syntax mode_default Syn_Ext.pure_ext empty_syntax;
 
 val basic_nonterms =
   (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",

--- a/src/Pure/Syntax/type_ext.ML	Wed Apr 06 21:55:41 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Apr 06 22:25:44 2011 +0200
@@ -15,7 +15,6 @@
 signature TYPE_EXT =
 sig
   include TYPE_EXT0
-  val type_ext: Syn_Ext.syn_ext
 end;
 
 structure Type_Ext: TYPE_EXT =
@@ -45,50 +44,4 @@
   | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
   | strip_positions_ast ast = ast;
 
-
-
-(** the type syntax **)
-
-fun typ c = Type (c, []);
-
-val class_nameT = typ "class_name";
-val type_nameT = typ "type_name";
-
-val sortT = typ "sort";
-val classesT = typ "classes";
-val typesT = typ "types";
-
-local open Lexicon Syn_Ext in
-
-val type_ext = syn_ext' false (K false)
-  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
-   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
-   Mfix ("_",           type_nameT --> typeT,          "", [], max_pri),
-   Mfix ("_",           idT --> type_nameT,            "_type_name", [], max_pri),
-   Mfix ("_",           longidT --> type_nameT,        "_type_name", [], max_pri),
-   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
-   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
-   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
-   Mfix ("_",           class_nameT --> sortT,         "", [], max_pri),
-   Mfix ("_",           idT --> class_nameT,           "_class_name", [], max_pri),
-   Mfix ("_",           longidT --> class_nameT,       "_class_name", [], max_pri),
-   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
-   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
-   Mfix ("_",           class_nameT --> classesT,      "", [], max_pri),
-   Mfix ("_,_",         [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
-   Mfix ("_ _",         [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
-   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
-   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
-   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
-   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
-   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
-   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
-   Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
-  ["_type_prop"]
-  ([], [], [], [])
-  []
-  ([], []);
-
 end;
-
-end;

--- a/src/Pure/pure_thy.ML	Wed Apr 06 21:55:41 2011 +0200
+++ b/src/Pure/pure_thy.ML	Wed Apr 06 22:25:44 2011 +0200
@@ -65,7 +65,31 @@
     (Binding.name "dummy", 0, NoSyn)]
   #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
   #> Sign.add_syntax_i
-   [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
+   [("",            typ "tid => type",                 Delimfix "_"),
+    ("",            typ "tvar => type",                Delimfix "_"),
+    ("",            typ "type_name => type",           Delimfix "_"),
+    ("_type_name",  typ "id => type_name",             Delimfix "_"),
+    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
+    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
+    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
+    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], Syntax.max_pri)),
+    ("",            typ "class_name => sort",          Delimfix "_"),
+    ("_class_name", typ "id => class_name",            Delimfix "_"),
+    ("_class_name", typ "longid => class_name",        Delimfix "_"),
+    ("_topsort",    typ "sort",                        Delimfix "{}"),
+    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
+    ("",            typ "class_name => classes",       Delimfix "_"),
+    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
+    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)),
+    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
+    ("",            typ "type => types",               Delimfix "_"),
+    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
+    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
+    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
+    ("",            typ "type => type",                Delimfix "'(_')"),
+    ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
+    ("_type_prop",  typ "'a",                          NoSyn),
+    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
     ("_abs",        typ "'a",                          NoSyn),
     ("",            typ "'a => args",                  Delimfix "_"),
     ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),