diff -r 538daee762e6 -r 593365d61ecc Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 12:15:14 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 12:23:02 2010 +0100
@@ -7,7 +7,7 @@
 
 signature QUOTIENT_DEF =
 sig
-  val quotient_def: mixfix -> Attrib.binding -> term -> term ->
+  val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) ->
     local_theory -> (term * thm) * local_theory
 
   val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) ->
@@ -37,8 +37,12 @@
    be a terms composed of constant. Similarly the
    left-hand side must be a single constant.
 *)
-fun quotient_def mx attr lhs rhs lthy =
+fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy =
 let
+  val mx =
+    case bindmx of
+      SOME (_, mx) => mx
+    | _ => NoSyn
   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
   val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
 
@@ -66,13 +70,12 @@
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in
-  case bindmx of
-    SOME (b, mx) => quotient_def mx attr lhs rhs lthy'' |> snd
-  | _ => quotient_def NoSyn attr lhs rhs lthy'' |> snd
+  quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |> snd
 end
 
+val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where"
 val quotdef_parser =
-  (Scan.option (OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where")) --
+  (Scan.option binding_mixfix_parser) --
     OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))
 
 val _ =