# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265986243 -3600
# Node ID 93c9022ba5e9f34bfb43e3138ab9f007ac21e8d4
# Parent  10a6ba364ce1b1b3db1b4d4b87b62e8dcc680184
"is" defined as the keyword

diff -r 10a6ba364ce1 -r 93c9022ba5e9 Quot/quotient_def.ML
--- 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"