1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 25 14:47:38 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Jul 25 15:01:18 2014 +0200
     1.3 @@ -154,11 +154,12 @@
     1.4  (* old-style defs *)
     1.5  
     1.6  fun add_defs ((unchecked, overloaded), args) thy =
     1.7 + (legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead";
     1.8    thy |>
     1.9      (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
    1.10        overloaded
    1.11        (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
    1.12 -  |> snd;
    1.13 +  |> snd);
    1.14  
    1.15  
    1.16  (* declarations *)