old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;

--- 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 *)