# HG changeset patch
# User wenzelm
# Date 1406293278 -7200
# Node ID cc0aa65288903ba14bf20909ae593e694e8d2354
# Parent  648c5ef4876d59b103ae6cc2e8df2577e4caf080
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;

diff -r 648c5ef4876d -r cc0aa6528890 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 25 14:47:38 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Jul 25 15:01:18 2014 +0200
@@ -154,11 +154,12 @@
 (* old-style defs *)
 
 fun add_defs ((unchecked, overloaded), args) thy =
+ (legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead";
   thy |>
     (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
       overloaded
       (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
-  |> snd;
+  |> snd);
 
 
 (* declarations *)