equal
deleted
inserted
replaced
150 |
150 |
151 (* type propositions *) |
151 (* type propositions *) |
152 |
152 |
153 fun mk_type ty = |
153 fun mk_type ty = |
154 Syntax.const "_constrain" $ |
154 Syntax.const "_constrain" $ |
155 Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); |
155 Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty); |
156 |
156 |
157 fun ofclass_tr [ty, cls] = cls $ mk_type ty |
157 fun ofclass_tr [ty, cls] = cls $ mk_type ty |
158 | ofclass_tr ts = raise TERM ("ofclass_tr", ts); |
158 | ofclass_tr ts = raise TERM ("ofclass_tr", ts); |
159 |
159 |
160 fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty |
160 fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty |