# HG changeset patch
# User wenzelm
# Date 1427230465 -3600
# Node ID 684cfaa12e47b09fac97fe80d93c95128279e565
# Parent  ca948c89828e9703280d97945f08205c04be6a37
clarified case_tac fixes and context;

diff -r ca948c89828e -r 684cfaa12e47 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 24 20:07:27 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 24 21:54:25 2015 +0100
@@ -244,7 +244,7 @@
        THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
 
 -- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] THEN_ALL_NEW
   (asm_full_simp_tac @{context})) 7*})
 
 apply (tactic "forward_hyp_tac @{context}")
diff -r ca948c89828e -r 684cfaa12e47 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 20:07:27 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 24 21:54:25 2015 +0100
@@ -131,7 +131,7 @@
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context = ctxt} =>
-                Induct_Tacs.case_tac ctxt "y" 1 THEN
+                Induct_Tacs.case_tac ctxt "y" [] 1 THEN
                 asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1
diff -r ca948c89828e -r 684cfaa12e47 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Mar 24 20:07:27 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Mar 24 21:54:25 2015 +0100
@@ -798,7 +798,7 @@
 fun split_idle_tac ctxt =
   SELECT_GOAL
    (TRY (rtac @{thm actionI} 1) THEN
-    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
+    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] 1 THEN
     rewrite_goals_tac ctxt @{thms action_rews} THEN
     forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
     asm_full_simp_tac ctxt 1);
diff -r ca948c89828e -r 684cfaa12e47 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Tue Mar 24 20:07:27 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Tue Mar 24 21:54:25 2015 +0100
@@ -6,8 +6,10 @@
 
 signature INDUCT_TACS =
 sig
-  val case_tac: Proof.context -> string -> int -> tactic
-  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
+  val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+    int -> tactic
+  val case_rule_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+    thm -> int -> tactic
   val induct_tac: Proof.context -> string option list list -> int -> tactic
   val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
 end
@@ -26,29 +28,35 @@
         quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
   in (u, U) end;
 
-fun gen_case_tac ctxt0 s opt_rule i st =
+fun gen_case_tac ctxt s fixes opt_rule i st =
   let
-    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
       (case opt_rule of
         SOME rule => rule
       | NONE =>
-          (case Induct.find_casesT ctxt
-              (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
-                Syntax.read_input_pos s))) of
-            rule :: _ => rule
-          | [] => @{thm case_split}));
+          let
+            val ctxt' = ctxt
+              |> Variable.focus_subgoal i st |> #2
+              |> Config.get ctxt Rule_Insts.schematic ?
+                  Proof_Context.set_mode Proof_Context.mode_schematic
+              |> Context_Position.set_visible false;
+            val t = Syntax.read_term ctxt' s;
+          in
+            (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, Syntax.read_input_pos s))) of
+              rule :: _ => rule
+            | [] => @{thm case_split})
+          end);
     val _ = Method.trace ctxt [rule];
 
     val xi =
       (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
         Var (xi, _) :: _ => xi
       | _ => raise THM ("Malformed cases rule", 0, [rule]));
-  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] [] rule i st end
+  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
   handle THM _ => Seq.empty;
 
-fun case_tac ctxt s = gen_case_tac ctxt s NONE;
-fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
+fun case_tac ctxt s xs = gen_case_tac ctxt s xs NONE;
+fun case_rule_tac ctxt s xs rule = gen_case_tac ctxt s xs (SOME rule);
 
 
 (* induction *)
@@ -130,8 +138,8 @@
 val _ =
   Theory.setup
    (Method.setup @{binding case_tac}
-      (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
-        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+      (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+        (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s xs r)))
       "unstructured case analysis on types" #>
     Method.setup @{binding induct_tac}
       (Args.goal_spec -- varss -- opt_rules >>