115 ("", typ "type_name \<Rightarrow> type", Mixfix.mixfix "_"), |
115 ("", typ "type_name \<Rightarrow> type", Mixfix.mixfix "_"), |
116 ("_type_name", typ "id \<Rightarrow> type_name", Mixfix.mixfix "_"), |
116 ("_type_name", typ "id \<Rightarrow> type_name", Mixfix.mixfix "_"), |
117 ("_type_name", typ "longid \<Rightarrow> type_name", Mixfix.mixfix "_"), |
117 ("_type_name", typ "longid \<Rightarrow> type_name", Mixfix.mixfix "_"), |
118 ("_ofsort", typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
118 ("_ofsort", typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
119 ("_ofsort", typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
119 ("_ofsort", typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
120 ("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_()::_", [0], 1000)), |
120 ("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_' ::_", [0], 1000)), |
121 ("", typ "class_name \<Rightarrow> sort", Mixfix.mixfix "_"), |
121 ("", typ "class_name \<Rightarrow> sort", Mixfix.mixfix "_"), |
122 ("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"), |
122 ("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"), |
123 ("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"), |
123 ("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"), |
124 ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), |
124 ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), |
125 ("_topsort", typ "sort", Mixfix.mixfix "{}"), |
125 ("_topsort", typ "sort", Mixfix.mixfix "{}"), |
140 ("", typ "'a \<Rightarrow> args", Mixfix.mixfix "_"), |
140 ("", typ "'a \<Rightarrow> args", Mixfix.mixfix "_"), |
141 ("_args", typ "'a \<Rightarrow> args \<Rightarrow> args", Mixfix.mixfix "_,/ _"), |
141 ("_args", typ "'a \<Rightarrow> args \<Rightarrow> args", Mixfix.mixfix "_,/ _"), |
142 ("", typ "id_position \<Rightarrow> idt", Mixfix.mixfix "_"), |
142 ("", typ "id_position \<Rightarrow> idt", Mixfix.mixfix "_"), |
143 ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), |
143 ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), |
144 ("_idtyp", typ "id_position \<Rightarrow> type \<Rightarrow> idt", mixfix ("_::_", [], 0)), |
144 ("_idtyp", typ "id_position \<Rightarrow> type \<Rightarrow> idt", mixfix ("_::_", [], 0)), |
145 ("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_()::_", [], 0)), |
145 ("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_' ::_", [], 0)), |
146 ("", typ "idt \<Rightarrow> idt", Mixfix.mixfix "'(_')"), |
146 ("", typ "idt \<Rightarrow> idt", Mixfix.mixfix "'(_')"), |
147 ("", typ "idt \<Rightarrow> idts", Mixfix.mixfix "_"), |
147 ("", typ "idt \<Rightarrow> idts", Mixfix.mixfix "_"), |
148 ("_idts", typ "idt \<Rightarrow> idts \<Rightarrow> idts", mixfix ("_/ _", [1, 0], 0)), |
148 ("_idts", typ "idt \<Rightarrow> idts \<Rightarrow> idts", mixfix ("_/ _", [1, 0], 0)), |
149 ("", typ "idt \<Rightarrow> pttrn", Mixfix.mixfix "_"), |
149 ("", typ "idt \<Rightarrow> pttrn", Mixfix.mixfix "_"), |
150 ("", typ "pttrn \<Rightarrow> pttrns", Mixfix.mixfix "_"), |
150 ("", typ "pttrn \<Rightarrow> pttrns", Mixfix.mixfix "_"), |