# HG changeset patch
# User wenzelm
# Date 1138881264 -3600
# Node ID e7d4e51bd4b1acd8b38c9b499ff43da83b58de3a
# Parent  a8e913c93578e7b66e61ee58b76ed6a371522093
tuned msg;

diff -r a8e913c93578 -r e7d4e51bd4b1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Feb 02 12:54:08 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Feb 02 12:54:24 2006 +0100
@@ -1108,7 +1108,7 @@
 local
 
 fun no_dups _ [] = ()
-  | no_dups ctxt dups = error ("Duplicate variable(s): " ^ commas_quote dups);
+  | no_dups ctxt dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
 
 fun gen_fixes prep raw_vars ctxt =
   let