diff -r 34f782641caa -r dcdfb6355a05 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Sep 13 21:06:58 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Sep 13 22:25:21 2015 +0200 @@ -1249,7 +1249,7 @@ val _ = if legacy then legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^ - " -- use proof method \"goals\" instead") + " -- use proof method \"goal_cases\" instead") else (); val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;