# HG changeset patch
# User wenzelm
# Date 1181685724 -7200
# Node ID df3d21caad2c4cc1e24da45a451c1c258573cd9f
# Parent  9e3c0c1ad0ad347aa944d6a020ccccaa1cb65aec
tuned msg;

diff -r 9e3c0c1ad0ad -r df3d21caad2c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 13 00:02:03 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 13 00:02:04 2007 +0200
@@ -475,7 +475,8 @@
     val is_declared = is_some (def_type (x, ~1));
     val res =
       if is_free andalso not is_internal then (no_skolem false x; sko)
-      else ((no_skolem false x; ()) handle ERROR msg => legacy_feature msg;
+      else ((no_skolem false x; ()) handle ERROR msg =>
+          legacy_feature (msg ^ ContextPosition.str_of ctxt);
         if is_internal andalso is_declared then SOME x else NONE);
   in if is_some res then res else if is_declared then SOME x else NONE end;