diff -r 85c6c2a1952d -r 48d935524988 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 11 11:48:24 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 11 15:07:15 2016 +0200
@@ -145,7 +145,7 @@
     val lhs = prep_term lhs_constraint raw_lhs
     val rhs = prep_term dummyT raw_rhs
 
-    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    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"
     val _ = if is_Const rhs then () else warning "The definiens is not a constant"