# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1266248268 -3600
# Node ID 2c84860c19d299a68db81ec5d9149d36d5982910
# Parent  689a18f9484cebbb5ebffbda73308ce0a969d2d4
small tuning

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