--- 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 "_,/ _"),