changeset 56243 | 2e10a36b8d46 |
parent 55948 | bb21b380f65d |
child 56245 | 84fc7dfa3cd4 |
--- a/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 12:14:33 2014 +0100 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 12:34:50 2014 +0100 @@ -152,7 +152,7 @@ fun mk_type ty = Syntax.const "_constrain" $ - Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty); + Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty); fun ofclass_tr [ty, cls] = cls $ mk_type ty | ofclass_tr ts = raise TERM ("ofclass_tr", ts);