# HG changeset patch
# User wenzelm
# Date 1441210450 -7200
# Node ID fc7ab11128dc99f6fedaa3d23cac19d6f6babc24
# Parent  30b0c4584244d0b770a5cc0256ed727902f3833e
tuned message;

diff -r 30b0c4584244 -r fc7ab11128dc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 02 17:25:14 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 02 18:14:10 2015 +0200
@@ -143,7 +143,8 @@
 (* old-style defs *)
 
 fun add_defs ((unchecked, overloaded), args) thy =
- (legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead";
+ (legacy_feature ("Old 'defs' command -- use 'definition' (with 'overloading') instead" ^
+    Position.here (Position.thread_data ()));
   thy |>
     (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
       overloaded