--- 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"