diff -r 84a38acbf512 -r 538daee762e6 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 12:15:14 2010 +0100
@@ -10,7 +10,7 @@
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     local_theory -> (term * thm) * local_theory
 
-  val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
+  val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> local_theory
 end;
 
@@ -59,24 +59,25 @@
   ((trm, thm), lthy'')
 end
 
-fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
+fun quotdef_cmd (bindmx, (attr, (lhs_str, rhs_str))) lthy =
 let
   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
-  quotient_def mx attr lhs rhs lthy'' |> snd
+  case bindmx of
+    SOME (b, mx) => quotient_def mx attr lhs rhs lthy'' |> snd
+  | _ => quotient_def NoSyn attr lhs rhs lthy'' |> snd
 end
 
 val quotdef_parser =
-  (SpecParse.opt_thm_name ":" --
-     OuterParse.term) --
-      (OuterParse.opt_mixfix' --| OuterParse.$$$ "is" --
-         OuterParse.term)
+  (Scan.option (OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where")) --
+    OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))
 
-val _ = OuterSyntax.local_theory "quotient_definition"
-	  "definition for constants over the quotient type"
-             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+val _ =
+  OuterSyntax.local_theory "quotient_definition"
+    "definition for constants over the quotient type"
+      OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd))
 
 end; (* structure *)