diff -r 689a18f9484c -r 2c84860c19d2 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 16:28:07 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 16:37:48 2010 +0100
@@ -38,9 +38,13 @@
    side must be a constant.
 *)
 fun error_msg bind str = 
+let 
+  val name = Binding.name_of bind
+  val pos = Position.str_of (Binding.pos_of bind)
+in
   error ("Head of quotient_definition " ^ 
-    (quote str) ^ " differs from declaration " ^ (Binding.name_of bind) ^
-      Position.str_of (Binding.pos_of bind))
+    (quote str) ^ " differs from declaration " ^ name ^ pos)
+end
 
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
 let