diff -r ce23193a42a4 -r 87a2624f57e4 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Nov 20 16:59:37 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Nov 20 17:04:59 2011 +0100
@@ -6,10 +6,12 @@
 
 signature QUOTIENT_DEF =
 sig
-  val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
+  val quotient_def:
+    (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
     local_theory -> Quotient_Info.quotconsts * local_theory
 
-  val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
+  val quotient_def_cmd:
+    (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> Quotient_Info.quotconsts * local_theory
 
   val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
@@ -85,10 +87,12 @@
 
 fun check_term' cnstr ctxt =
   Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
-fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
+
+fun read_term' cnstr ctxt =
+  check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
 
 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
-val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
+val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
 
 
 (* a wrapper for automatically lifting a raw constant *)
@@ -109,6 +113,6 @@
 val _ =
   Outer_Syntax.local_theory "quotient_definition"
     "definition for constants over the quotient type"
-      Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
+      Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
 
 end; (* structure *)