# HG changeset patch
# User wenzelm
# Date 1537732171 -7200
# Node ID 8c240fdeffcb4b8d1364a0d1c2ada8e4d03379f2
# Parent  364c989edb492f8a589a9c293b089e88e7764c71
discontinued old-style goal cases;

diff -r 364c989edb49 -r 8c240fdeffcb NEWS
--- a/NEWS	Sun Sep 23 21:38:30 2018 +0200
+++ b/NEWS	Sun Sep 23 21:49:31 2018 +0200
@@ -18,6 +18,10 @@
 * More robust treatment of structural errors: begin/end blocks take
 precedence over goal/proof.
 
+* Implicit cases goal1, goal2, goal3, etc. have been discontinued
+(legacy feature since Isabelle2016).
+
+
 
 *** HOL ***
 
diff -r 364c989edb49 -r 8c240fdeffcb src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Sep 23 21:38:30 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Sep 23 21:49:31 2018 +0200
@@ -415,24 +415,11 @@
 
 local
 
-fun goalN i = "goal" ^ string_of_int i;
-fun goals st = map goalN (1 upto Thm.nprems_of st);
-
-fun no_goal_cases st = map (rpair NONE) (goals st);
-
-fun goal_cases ctxt st =
-  Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
-
 fun apply_method text ctxt state =
   find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
     Method.evaluate text ctxt using (goal_ctxt, goal)
     |> Seq.map_result (fn (goal_ctxt', goal') =>
-      let
-        val goal_ctxt'' = goal_ctxt'
-          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
-        val state' = state
-          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
-      in state' end));
+        state |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed))));
 
 in
 
diff -r 364c989edb49 -r 8c240fdeffcb src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 23 21:38:30 2018 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 23 21:49:31 2018 +0200
@@ -151,9 +151,8 @@
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
+  val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
-  val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
@@ -228,7 +227,7 @@
 
 (** Isar proof context information **)
 
-type cases = (Rule_Cases.T * {legacy: bool}) Name_Space.table;
+type cases = Rule_Cases.T Name_Space.table;
 val empty_cases: cases = Name_Space.empty_table Markup.caseN;
 
 datatype data =
@@ -238,7 +237,7 @@
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts, based on initial global facts*)
-    cases: cases};               (*named case contexts: case, legacy, running index*)
+    cases: cases};               (*named case contexts*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
   Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -1319,17 +1318,10 @@
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-fun update_case _ _ ("", _) cases = cases
-  | update_case _ _ (name, NONE) cases = Name_Space.del_table name cases
-  | update_case context legacy (name, SOME c) cases =
-      let
-        val binding = Binding.name name |> legacy ? Binding.concealed;
-        val (_, cases') = Name_Space.define context false (binding, (c, {legacy = legacy})) cases;
-      in cases' end;
-
-fun update_cases' legacy args ctxt =
-  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
-  in map_cases (fold (update_case context legacy) args) ctxt end;
+fun update_case _ ("", _) cases = cases
+  | update_case _ (name, NONE) cases = Name_Space.del_table name cases
+  | update_case context (name, SOME c) cases =
+      #2 (Name_Space.define context false (Binding.name name, c) cases);
 
 fun fix (b, T) ctxt =
   let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
@@ -1337,8 +1329,9 @@
 
 in
 
-val update_cases = update_cases' false;
-val update_cases_legacy = update_cases' true;
+fun update_cases args ctxt =
+  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
+  in map_cases (fold (update_case context) args) ctxt end;
 
 fun case_result c ctxt =
   let
@@ -1356,13 +1349,8 @@
 
 fun check_case ctxt internal (name, pos) param_specs =
   let
-    val (_, (Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy})) =
+    val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
-    val _ =
-      if legacy then
-        legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
-          " -- use proof method \"goal_cases\" instead")
-      else ();
 
     val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
@@ -1537,10 +1525,9 @@
 
 fun pretty_cases ctxt =
   let
-    fun mk_case (_, (_, {legacy = true})) = NONE
-      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
-          SOME (name, (fixes, case_result c ctxt));
-    val cases = dest_cases NONE ctxt |> map_filter mk_case;
+    val cases =
+      dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
+        (name, (fixes, case_result c ctxt)));
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]
@@ -1563,20 +1550,18 @@
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
 
-    fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
-      if legacy then NONE
-      else
-        let
-          val concl =
-            if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
-            then Rule_Cases.case_conclN else Auto_Bind.thesisN;
-        in
-          SOME (cat_lines
-            ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
-             "  then show ?" ^ concl ^ " sorry"])
-        end;
+    fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
+      let
+        val concl =
+          if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
+          then Rule_Cases.case_conclN else Auto_Bind.thesisN;
+      in
+        cat_lines
+          ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
+           "  then show ?" ^ concl ^ " sorry"]
+      end;
   in
-    (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
+    (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
       [] => ""
     | proofs =>
         "Proof outline with cases:\n" ^