diff -r 2cb5745f403e -r 7be9b054f672 Quot/quotient_typ.ML --- 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