changeset 918 | 7be9b054f672 |
parent 885 | fe7d27e197e5 |
child 952 | 9c3b3eaecaff |
--- a/Quot/quotient_typ.ML Sat Jan 23 17:25:18 2010 +0100 +++ b/Quot/quotient_typ.ML Sun Jan 24 23:41:27 2010 +0100 @@ -264,6 +264,8 @@ let fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = let + (*val rty = Syntax.read_typ lthy rty_str*) + val rty = Syntax.read_typ lthy rty_str val rel = Syntax.read_term lthy rel_str in