--- 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.
--- 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