Quot/quotient_typ.ML
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