262            

   262            

   263 fun quotient_type_cmd specs lthy = 

   263 fun quotient_type_cmd specs lthy = 

   264 let

   264 let

   265   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =

   265   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =

   266   let

   266   let

   267     val rty = Syntax.read_typ lthy rty_str

   269     val rty = Syntax.read_typ lthy rty_str

   268     val rel = Syntax.read_term lthy rel_str 

   270     val rel = Syntax.read_term lthy rel_str 

   269   in

   271   in

   270     ((vs, qty_name, mx), (rty, rel))

   272     ((vs, qty_name, mx), (rty, rel))

   271   end

   273   end