diff -r aaeb5a34d21a -r 3c8ad149a4d3 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Feb 12 16:06:09 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Feb 12 16:27:25 2010 +0100
@@ -71,7 +71,8 @@
 
 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
 let
-  val [lhs, rhs] = Syntax.read_terms lthy [lhs_str, rhs_str]
+  val lhs = Syntax.read_term lthy lhs_str
+  val rhs = Syntax.read_term lthy rhs_str
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in