src/Pure/pure_thy.ML
changeset 42263 49b1b8d0782f
parent 42245 29e3967550d5
child 42284 326f57825e1a
     1.1 --- a/src/Pure/pure_thy.ML	Wed Apr 06 21:55:41 2011 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 06 22:25:44 2011 +0200
     1.3 @@ -65,7 +65,31 @@
     1.4      (Binding.name "dummy", 0, NoSyn)]
     1.5    #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
     1.6    #> Sign.add_syntax_i
     1.7 -   [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
     1.8 +   [("",            typ "tid => type",                 Delimfix "_"),
     1.9 +    ("",            typ "tvar => type",                Delimfix "_"),
    1.10 +    ("",            typ "type_name => type",           Delimfix "_"),
    1.11 +    ("_type_name",  typ "id => type_name",             Delimfix "_"),
    1.12 +    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
    1.13 +    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
    1.14 +    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
    1.15 +    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], Syntax.max_pri)),
    1.16 +    ("",            typ "class_name => sort",          Delimfix "_"),
    1.17 +    ("_class_name", typ "id => class_name",            Delimfix "_"),
    1.18 +    ("_class_name", typ "longid => class_name",        Delimfix "_"),
    1.19 +    ("_topsort",    typ "sort",                        Delimfix "{}"),
    1.20 +    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
    1.21 +    ("",            typ "class_name => classes",       Delimfix "_"),
    1.22 +    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
    1.23 +    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)),
    1.24 +    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    1.25 +    ("",            typ "type => types",               Delimfix "_"),
    1.26 +    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
    1.27 +    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
    1.28 +    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
    1.29 +    ("",            typ "type => type",                Delimfix "'(_')"),
    1.30 +    ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
    1.31 +    ("_type_prop",  typ "'a",                          NoSyn),
    1.32 +    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
    1.33      ("_abs",        typ "'a",                          NoSyn),
    1.34      ("",            typ "'a => args",                  Delimfix "_"),
    1.35      ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),