# HG changeset patch
# User wenzelm
# Date 1435268945 -7200
# Node ID d2fbc021a44d3fff88f13c611f5b5e9428a3bed9
# Parent  7e741e22d7fc54f94c12a912be51cecf8bbf4ba9
implicit goal cases are legacy;

diff -r 7e741e22d7fc -r d2fbc021a44d NEWS
--- a/NEWS	Thu Jun 25 23:33:47 2015 +0200
+++ b/NEWS	Thu Jun 25 23:49:05 2015 +0200
@@ -80,6 +80,10 @@
 * Proof method "goals" turns the current subgoals into cases within the
 context; the conclusion is bound to variable ?case in each case.
 
+* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
+is marked as legacy, and will be removed eventually. Note that proof
+method "goals" achieves a similar effect within regular Isar.
+
 * Nesting of Isar goal structure has been clarified: the context after
 the initial backwards refinement is retained for the whole proof, within
 all its context sections (as indicated via 'next'). This is e.g.
diff -r 7e741e22d7fc -r d2fbc021a44d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jun 25 23:33:47 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jun 25 23:49:05 2015 +0200
@@ -1245,7 +1245,11 @@
   let
     val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
-    val _ = if legacy then Context_Position.report ctxt pos Markup.improper else ();
+    val _ =
+      if legacy then
+        legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
+          " -- use proof method \"goals\" instead")
+      else ();
 
     val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys