--- a/Quot/quotient_def.ML	Fri Feb 12 12:06:09 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Feb 12 15:50:43 2010 +0100
@@ -71,20 +71,17 @@
 
 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
 let
-  val lhs = Syntax.read_term lthy lhs_str
-  val rhs = Syntax.read_term lthy rhs_str
+  val [lhs, rhs] = Syntax.read_terms lthy [lhs_str, rhs_str]
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in
   quotient_def mx attr lhs rhs lthy'' |> snd
 end
 
-val _ = OuterKeyword.keyword "as";
-
 val quotdef_parser =
   (SpecParse.opt_thm_name ":" --
      OuterParse.term) --
-      (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+      (OuterParse.opt_mixfix' --| OuterParse.$$$ "is" --
          OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_definition"