# HG changeset patch
# User wenzelm
# Date 1450042385 -3600
# Node ID 00b70452dc7fc2cb1125061ac25b94d035a59320
# Parent  c601d3c76362235c66469b9c551e90d2666910b9# Parent  4d3527b94f2ac369d5d2e0cac8f16dba05271064
merged

diff -r c601d3c76362 -r 00b70452dc7f NEWS
--- a/NEWS	Sat Dec 12 18:58:06 2015 +0100
+++ b/NEWS	Sun Dec 13 22:33:05 2015 +0100
@@ -626,6 +626,12 @@
 
 *** ML ***
 
+* Isar proof methods are based on a slightly more general type
+context_tactic, which allows to change the proof context dynamically
+(e.g. to update cases) and indicate explicit Seq.Error results. Former
+METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
+provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
+
 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
 
 * The auxiliary module Pure/display.ML has been eliminated. Its
diff -r c601d3c76362 -r 00b70452dc7f src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy	Sun Dec 13 22:33:05 2015 +0100
@@ -165,12 +165,12 @@
 
 section \<open>Proof methods\<close>
 
-text \<open>A \<open>method\<close> is a function \<open>context \<rightarrow> thm\<^sup>* \<rightarrow> goal
-  \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*\<close> that operates on the full Isar goal
-  configuration with context, goal facts, and tactical goal state and
-  enumerates possible follow-up goal states, with the potential
-  addition of named extensions of the proof context (\<^emph>\<open>cases\<close>).
-  The latter feature is rarely used.
+text \<open>
+  A \<open>method\<close> is a function \<open>thm\<^sup>* \<rightarrow> context * goal \<rightarrow> (context \<times> goal)\<^sup>*\<^sup>*\<close>
+  that operates on the full Isar goal configuration with context, goal facts,
+  and tactical goal state and enumerates possible follow-up goal states. Under
+  normal circumstances, the goal context remains unchanged, but it is also
+  possible to declare named extensions of the proof context (\<^emph>\<open>cases\<close>).
 
   This means a proof method is like a structurally enhanced tactic
   (cf.\ \secref{sec:tactics}).  The well-formedness conditions for
@@ -287,11 +287,11 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type Proof.method} \\
-  @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\
+  @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
   @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
   @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
   @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
-  @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
+  @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
   @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
   string -> theory -> theory"} \\
   \end{mldecls}
@@ -299,9 +299,11 @@
   \<^descr> Type @{ML_type Proof.method} represents proof methods as
   abstract type.
 
-  \<^descr> @{ML METHOD_CASES}~\<open>(fn facts => cases_tactic)\<close> wraps
-  \<open>cases_tactic\<close> depending on goal facts as proof method with
-  cases; the goal context is passed via method syntax.
+  \<^descr> @{ML CONTEXT_METHOD}~\<open>(fn facts => context_tactic)\<close> wraps \<open>context_tactic\<close>
+  depending on goal facts as a general proof method that may change the proof
+  context dynamically. A typical operation is @{ML
+  Proof_Context.update_cases}, which is wrapped up as combinator @{index_ML
+  CONTEXT_CASES} for convenience.
 
   \<^descr> @{ML METHOD}~\<open>(fn facts => tactic)\<close> wraps \<open>tactic\<close> depending on goal facts as regular proof method; the goal
   context is passed via method syntax.
@@ -315,7 +317,7 @@
   addresses a specific subgoal as simple proof method that operates on
   subgoal 1.  Goal facts are inserted into the subgoal then the \<open>tactic\<close> is applied.
 
-  \<^descr> @{ML Method.insert_tac}~\<open>facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>.  This is convenient to reproduce
+  \<^descr> @{ML Method.insert_tac}~\<open>ctxt facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>.  This is convenient to reproduce
   part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping
   within regular @{ML METHOD}, for example.
 
@@ -348,7 +350,7 @@
   have "A \<and> B"
     using a and b
     ML_val \<open>@{Isar.goal}\<close>
-    apply (tactic \<open>Method.insert_tac facts 1\<close>)
+    apply (tactic \<open>Method.insert_tac @{context} facts 1\<close>)
     apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>)
     done
 end
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -76,14 +76,13 @@
 type match_args = {multi : bool, cut : int};
 
 val parse_match_args =
-  Scan.optional (Args.parens (Parse.enum1 ","
-    (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.nat 1))) [] >>
-    (fn ss =>
-      fold (fn s => fn {multi, cut} =>
-        (case s of
-          ("multi", _) => {multi = true, cut = cut}
-        | ("cut", n) => {multi = multi, cut = n}))
-      ss {multi = false, cut = ~1});
+  Scan.optional
+    (Args.parens
+      (Parse.enum1 ","
+        (Args.$$$ "multi" >> (fn _ => fn {cut, ...} => {multi = true, cut = cut}) ||
+         Args.$$$ "cut" |-- Scan.optional Parse.nat 1
+          >> (fn n => fn {multi, ...} => {multi = multi, cut = n})))) []
+  >> (fn fs => fold I fs {multi = false, cut = ~1});
 
 fun parse_named_pats match_kind =
   Args.context --
@@ -295,9 +294,6 @@
     (text', ctxt')
   end;
 
-fun DROP_CASES (tac: cases_tactic) : tactic =
-  tac #> Seq.map (fn (_, st) => st);
-
 fun prep_fact_pat ((x, args), pat) ctxt =
   let
     val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
@@ -313,18 +309,6 @@
     ((((Option.map prep_head x, args), params''), pat''), ctxt')
   end;
 
-fun recalculate_maxidx env =
-  let
-    val tenv = Envir.term_env env;
-    val tyenv = Envir.type_env env;
-    val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
-    val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
-  in
-    Envir.Envir
-      {maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env),
-        tenv = tenv, tyenv = tyenv}
-  end
-
 fun morphism_env morphism env =
   let
     val tenv = Envir.term_env env
@@ -663,7 +647,7 @@
     |> Seq.map (apsnd (morphism_env morphism))
   end;
 
-fun real_match using ctxt fixes m text pats goal =
+fun real_match using goal_ctxt fixes m text pats st =
   let
     fun make_fact_matches ctxt get =
       let
@@ -675,10 +659,9 @@
 
     fun make_term_matches ctxt get =
       let
-        val pats' =
-          map
-            (fn ((SOME _, _), _) => error "Cannot name term match"
-              | ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats;
+        val pats' = map
+          (fn ((SOME _, _), _) => error "Cannot name term match"
+            | ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats;
 
         val thm_of = Drule.mk_term o Thm.cterm_of ctxt;
         fun get' t = get (Logic.dest_term t) |> map thm_of;
@@ -689,13 +672,17 @@
   in
     (case m of
       Match_Fact net =>
-        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal)
-          (make_fact_matches ctxt (Item_Net.retrieve net))
+        make_fact_matches goal_ctxt (Item_Net.retrieve net)
+        |> Seq.map (fn (text, ctxt') =>
+          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+          |> Seq.filter_results |> Seq.map snd)
     | Match_Term net =>
-        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal)
-          (make_term_matches ctxt (Item_Net.retrieve net))
+        make_term_matches goal_ctxt (Item_Net.retrieve net)
+        |> Seq.map (fn (text, ctxt') =>
+          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+          |> Seq.filter_results |> Seq.map snd)
     | match_kind =>
-        if Thm.no_prems goal then Seq.empty
+        if Thm.no_prems st then Seq.empty
         else
           let
             fun focus_cases f g =
@@ -704,10 +691,10 @@
               | Match_Concl => g
               | _ => raise Fail "Match kind fell through");
 
-            val (goal_thins, goal) = get_thinned_prems goal;
+            val (goal_thins, st') = get_thinned_prems st;
 
             val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
-              focus_cases (K Subgoal.focus_prems) focus_concl ctxt 1 NONE goal
+              focus_cases (K Subgoal.focus_prems) focus_concl goal_ctxt 1 NONE st'
               |>> augment_focus;
 
             val texts =
@@ -719,14 +706,15 @@
                      #> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids)
                      #> order_list))
                 (fn _ =>
-                  make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
+                  make_term_matches focus_ctxt
+                    (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
                 ();
 
             (*TODO: How to handle cases? *)
 
-            fun do_retrofit inner_ctxt goal' =
+            fun do_retrofit inner_ctxt st1 =
               let
-                val (goal'_thins, goal') = get_thinned_prems goal';
+                val (goal_thins', st2) = get_thinned_prems st1;
 
                 val thinned_prems =
                   ((subtract (eq_fst (op =))
@@ -739,68 +727,63 @@
 
                 val all_thinned_prems =
                   thinned_prems @
-                  map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins);
+                    map (fn (id, prem) => (id, (NONE, SOME prem))) (goal_thins' @ goal_thins);
 
                 val (thinned_local_prems, thinned_extra_prems) =
                   List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems;
 
                 val local_thins =
-                  thinned_local_prems
-                  |> map (fn (_, (SOME t, _)) => Thm.term_of t
-                           | (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term);
+                  thinned_local_prems |> map
+                    (fn (_, (SOME t, _)) => Thm.term_of t
+                      | (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term);
 
                 val extra_thins =
-                  thinned_extra_prems
-                  |> map (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of)
-                           | (id, (_, SOME pt)) => (id, pt))
+                  thinned_extra_prems |> map
+                    (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of)
+                      | (id, (_, SOME pt)) => (id, pt))
                   |> map (hyp_from_ctermid inner_ctxt);
 
-                val n_subgoals = Thm.nprems_of goal';
+                val n_subgoals = Thm.nprems_of st2;
                 fun prep_filter t =
                   Term.subst_bounds (map (Thm.term_of o snd) params |> rev, Term.strip_all_body t);
                 fun filter_test prems t =
                   if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE;
               in
-                Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |>
-                (if n_subgoals = 0 orelse null local_thins then I
-                 else
-                  Seq.map (Goal.restrict 1 n_subgoals)
-                  #> Seq.maps (ALLGOALS (fn i =>
-                      DETERM (filter_prems_tac' ctxt prep_filter filter_test local_thins i)))
-                  #> Seq.map (Goal.unrestrict 1))
-                  |> Seq.map (fold Thm.weaken extra_thins)
+                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st2 st
+                |> (n_subgoals > 0 andalso not (null local_thins)) ?
+                    (Seq.map (Goal.restrict 1 n_subgoals)
+                      #> Seq.maps (ALLGOALS (fn i =>
+                          DETERM (filter_prems_tac' goal_ctxt prep_filter filter_test local_thins i)))
+                      #> Seq.map (Goal.unrestrict 1))
+                |> Seq.map (fold Thm.weaken extra_thins)
               end;
 
             fun apply_text (text, ctxt') =
-              let
-                val goal' =
-                  DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
-                  |> Seq.maps (DETERM (do_retrofit ctxt'))
-                  |> Seq.map (fn goal => ([]: cases, goal));
-              in goal' end;
-          in
-            Seq.map apply_text texts
-          end)
+              Method.NO_CONTEXT_TACTIC ctxt'
+                (Method_Closure.method_evaluate text ctxt' using) focused_goal
+              |> Seq.maps (DETERM (do_retrofit ctxt'));
+          in Seq.map apply_text texts end)
   end;
 
-val match_parser =
-  parse_match_kind :-- (fn kind =>
-      Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
-    (fn (matches, bodies) => fn ctxt => fn using =>
-      Method.RUNTIME (fn st =>
-        let
-          fun exec (pats, fixes, text) goal =
-            let
-              val ctxt' =
-                fold Variable.declare_term fixes ctxt
-                |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
-            in real_match using ctxt' fixes matches text pats goal end;
-        in Seq.flat (Seq.FIRST (map exec bodies) st) end));
-
 val _ =
   Theory.setup
     (Method.setup @{binding match}
-      (match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt)))
+      (parse_match_kind :--
+        (fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
+        (fn (matches, bodies) => fn ctxt =>
+          CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
+            let
+              fun exec (pats, fixes, text) st' =
+                let
+                  val ctxt' =
+                    fold Variable.declare_term fixes ctxt
+                    (*FIXME Is this a good idea? We really only care about the maxidx*)
+                    |> fold (fn (_, t) => Variable.declare_term t) pats;
+                in real_match using ctxt' fixes matches text pats st' end;
+            in
+              Seq.flat (Seq.FIRST (map exec bodies) st)
+              |> Method.CONTEXT goal_ctxt
+            end))))
       "structural analysis/matching on goals");
 
 end;
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Filter.thy	Sun Dec 13 22:33:05 2015 +0100
@@ -233,24 +233,23 @@
   frequently_imp_iff
 
 ML \<open>
-  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
-    let
-      val mp_thms = facts RL @{thms eventually_rev_mp}
-      val raw_elim_thm =
-        (@{thm allI} RS @{thm always_eventually})
-        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
-        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
-      val cases_prop =
-        Thm.prop_of
-          (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
-      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
-    in
-      CASES cases (resolve_tac ctxt [raw_elim_thm] i)
-    end)
+  fun eventually_elim_tac facts =
+    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+      let
+        val mp_thms = facts RL @{thms eventually_rev_mp}
+        val raw_elim_thm =
+          (@{thm allI} RS @{thm always_eventually})
+          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+          |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+        val cases_prop =
+          Thm.prop_of
+            (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
+        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
+      in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end)
 \<close>
 
 method_setup eventually_elim = \<open>
-  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
+  Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1))
 \<close> "elimination of eventually quantifiers"
 
 subsubsection \<open>Finer-than relation\<close>
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Fun_Def.thy	Sun Dec 13 22:33:05 2015 +0100
@@ -103,7 +103,7 @@
 ML_file "Tools/Function/induction_schema.ML"
 
 method_setup induction_schema = \<open>
-  Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac)
+  Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
 \<close> "prove an induction principle"
 
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -154,7 +154,7 @@
 fun can_apply time tac st =
   let
     val {context = ctxt, facts, goal} = Proof.goal st
-    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
+    val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
   in
     (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
       SOME (SOME _) => true
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -5,9 +5,9 @@
 
 structure NominalInduct:
 sig
-  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+  val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
-    thm list -> int -> Rule_Cases.cases_tactic
+    thm list -> int -> context_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 struct
@@ -81,7 +81,7 @@
 
 (* nominal_induct_tac *)
 
-fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
+fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
   let
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
@@ -94,8 +94,8 @@
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
       in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
-  in
-    (fn i => fn st =>
+
+    fun context_tac _ _ =
       rules
       |> inst_mutual_rule ctxt insts avoiding
       |> Rule_Cases.consume ctxt (flat defs) facts
@@ -108,7 +108,7 @@
               val xs = nth_list fixings (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
-              Method.insert_tac (more_facts @ adefs) THEN'
+              Method.insert_tac ctxt (more_facts @ adefs) THEN'
                 (if simp then
                    Induct.rotate_tac k (length adefs) THEN'
                    Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
@@ -120,13 +120,13 @@
             Induct.guess_instance ctxt
               (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
-              CASES (rule_cases ctxt rule' cases)
+              CONTEXT_CASES (rule_cases ctxt rule' cases)
                 (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
-                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
-    THEN_ALL_NEW_CASES
+                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
+  in
+    (context_tac CONTEXT_THEN_ALL_NEW
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
-        else K all_tac)
-       THEN_ALL_NEW Induct.rulify_tac ctxt)
+        else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
   end;
 
 
@@ -169,8 +169,8 @@
   Scan.lift (Args.mode Induct.no_simpN) --
   (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
     avoiding -- fixing -- rule_spec) >>
-  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
-    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
+  (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
+    (nominal_induct_tac (not no_simp) x y z w facts 1));
 
 end;
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -372,11 +372,10 @@
           |> snd
         end)
       [goals] |>
-    Proof.apply (Method.Basic (fn ctxt => fn _ =>
-      EMPTY_CASES
+    Proof.refine_singleton (Method.Basic (fn ctxt => fn _ =>
+      Method.CONTEXT_TACTIC
        (rewrite_goals_tac ctxt defs_thms THEN
-        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
-    Seq.hd
+        compose_tac ctxt (false, rule, length rule_prems) 1)))
   end;
 
 in
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Partial_Function.thy	Sun Dec 13 22:33:05 2015 +0100
@@ -443,7 +443,7 @@
 
 declaration \<open>Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
-  (SOME @{thm fixp_induct_tailrec[where c=undefined]})\<close>
+  (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
 
 declaration \<open>Partial_Function.init "option" @{term option.fixp_fun}
   @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -1706,8 +1706,7 @@
       (lthy
        |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
          (map (single o rpair []) goals @ nontriv_wit_goals)
-       |> Proof.refine (Method.primitive_text (K I))
-       |> Seq.hd)
+       |> Proof.refine_singleton (Method.primitive_text (K I)))
   end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
     NONE Binding.empty Binding.empty [] raw_csts;
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -319,7 +319,7 @@
       unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
       unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
       EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
-        Method.insert_tac inserts, REPEAT_DETERM o dtac ctxt meta_spec,
+        Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
         REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
         if live = 1 then K all_tac
         else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -1579,8 +1579,7 @@
 val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
   lthy
   |> Proof.theorem NONE after_qed goalss
-  |> Proof.refine (Method.primitive_text (K I))
-  |> Seq.hd) ooo primcorec_ursive_cmd false;
+  |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
 
 val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
     lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -54,7 +54,7 @@
   assume_tac ctxt;
 
 fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
-  HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
+  HEADGOAL (Method.insert_tac ctxt exhaust_discs THEN' clean_blast_tac ctxt);
 
 fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   let val ks = 1 upto n in
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -1082,7 +1082,7 @@
 fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
   let val n = length in_rels;
   in
-    Method.insert_tac CIHs 1 THEN
+    Method.insert_tac ctxt CIHs 1 THEN
     unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
     REPEAT_DETERM (etac ctxt exE 1) THEN
     CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -356,7 +356,7 @@
   let
     val n = length card_of_min_algs;
   in
-    EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
+    EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
       REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
       rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
       rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -345,10 +345,9 @@
   (fn (goals, after_qed, definitions, lthy) =>
     lthy
     |> Proof.theorem NONE after_qed (map (single o rpair []) goals)
-    |> Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
-    |> Seq.hd
-    |> Proof.refine (Method.primitive_text (K I))
-    |> Seq.hd) oo
+    |> Proof.refine_singleton
+        (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
+    |> Proof.refine_singleton (Method.primitive_text (K I))) oo
   prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME));
 
 fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs =
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -171,7 +171,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+    |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
 val function =
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -121,7 +121,7 @@
 
         fun prep_subgoal_tac i =
           REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
-          THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
+          THEN Method.insert_tac ctxt (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
           THEN propagate_tac ctxt i
           THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
           THEN bool_subst_tac ctxt i;
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -345,7 +345,7 @@
 
 fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
   (* FIXME proper use of facts!? *)
-  (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
+  (ALLGOALS (Method.insert_tac ctxt facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
   let
     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -62,8 +62,6 @@
 
 (*** Automated monotonicity proofs ***)
 
-fun strip_cases ctac = ctac #> Seq.map snd;
-
 (*rewrite conclusion with k-th assumtion*)
 fun rewrite_with_asm_tac ctxt k =
   Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
@@ -95,7 +93,7 @@
        | SOME (arg, conv) =>
            let open Conv in
               if Term.is_open arg then no_tac
-              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
+              else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                 THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
                 THEN_ALL_NEW (CONVERSION
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -407,7 +407,7 @@
       by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
 
     fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
-        (Method.insert_tac wits THEN' 
+        (Method.insert_tac ctxt wits THEN' 
          eq_onp_to_top_tac ctxt THEN' (* normalize *)
          rtac ctxt unfold_lift_sel_rsp THEN'
          case_tac exhaust_rule ctxt THEN_ALL_NEW (
@@ -559,7 +559,7 @@
         val TFrees = Term.add_tfreesT qty []
 
         fun non_empty_typedef_tac non_empty_pred ctxt i =
-          (Method.insert_tac [non_empty_pred] THEN' 
+          (Method.insert_tac ctxt [non_empty_pred] THEN' 
             SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
         val uTname = unique_Tname (rty, qty)
         val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -272,7 +272,7 @@
 
 fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
   let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
-    HEADGOAL (Method.insert_tac nonschem_facts THEN'
+    HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
       CHANGED_PROP o metis_tac (these override_type_encs)
         (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   end
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -870,7 +870,7 @@
     val simpset_ctxt =
       put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
   in
-    Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}))
+    Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}))
     THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     THEN_ALL_NEW simp_tac simpset_ctxt
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -133,7 +133,7 @@
 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
 
 fun prop_tac ctxt prems =
-  Method.insert_tac prems
+  Method.insert_tac ctxt prems
   THEN' SUBGOAL (fn (prop, i) =>
     if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
     else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
@@ -324,7 +324,7 @@
   by fast+}
 
 fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
-  Method.insert_tac thms
+  Method.insert_tac ctxt thms
   THEN' (Classical.fast_tac ctxt'
     ORELSE' dresolve_tac ctxt cong_dest_rules
     THEN' Classical.fast_tac ctxt'))
@@ -615,7 +615,7 @@
 (* theory lemmas *)
 
 fun arith_th_lemma_tac ctxt prems =
-  Method.insert_tac prems
+  Method.insert_tac ctxt prems
   THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
   THEN' Arith_Data.arith_tac ctxt
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -114,7 +114,7 @@
   end
 
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
-  Method.insert_tac local_facts THEN'
+  Method.insert_tac ctxt local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
     let
@@ -131,7 +131,7 @@
   | Simp_Size_Method =>
     Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
   | _ =>
-    Method.insert_tac global_facts THEN'
+    Method.insert_tac ctxt global_facts THEN'
     (case meth of
       SATx_Method => SAT.satx_tac ctxt
     | Blast_Method => blast_tac ctxt
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/arith_data.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -48,8 +48,8 @@
       (Scan.succeed (fn ctxt =>
         METHOD (fn facts =>
           HEADGOAL
-          (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
-            THEN' arith_tac ctxt))))
+            (Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+              THEN' arith_tac ctxt))))
       "various arithmetic decision procedures");
 
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/coinduction.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -8,7 +8,7 @@
 
 signature COINDUCTION =
 sig
-  val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
+  val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic
 end;
 
 structure Coinduction : COINDUCTION =
@@ -37,85 +37,85 @@
     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
   end;
 
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _) =>
-  let
-    val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
-    fun find_coinduct t =
-      Induct.find_coinductP ctxt t @
-      (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
-    val raw_thm =
-      (case opt_raw_thm of
-        SOME raw_thm => raw_thm
-      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
-    val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
-    val cases = Rule_Cases.get raw_thm |> fst
-  in
-    HEADGOAL (
-      Object_Logic.rulify_tac ctxt THEN'
-      Method.insert_tac prems THEN'
-      Object_Logic.atomize_prems_tac ctxt THEN'
-      DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
-        let
-          val vars = raw_vars @ map (Thm.term_of o snd) params;
-          val names_ctxt = ctxt
-            |> fold Variable.declare_names vars
-            |> fold Variable.declare_thm (raw_thm :: prems);
-          val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
-          val (instT, inst) = Thm.match (thm_concl, concl);
-          val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
-          val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
-          val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
-            |> map (subst_atomic_types rhoTs);
-          val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
-          val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
-            |>> (fn names => Variable.variant_fixes names names_ctxt) ;
-          val eqs =
-            @{map 3} (fn name => fn T => fn (_, rhs) =>
-              HOLogic.mk_eq (Free (name, T), rhs))
-            names Ts raw_eqs;
-          val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
-            |> try (Library.foldr1 HOLogic.mk_conj)
-            |> the_default @{term True}
-            |> Ctr_Sugar_Util.list_exists_free vars
-            |> Term.map_abs_vars (Variable.revert_fixed ctxt)
-            |> fold_rev Term.absfree (names ~~ Ts)
-            |> Thm.cterm_of ctxt;
-          val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
-          val e = length eqs;
-          val p = length prems;
-        in
-          HEADGOAL (EVERY' [resolve_tac ctxt [thm],
-            EVERY' (map (fn var =>
-              resolve_tac ctxt
-                [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
-            if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
-            else
-              REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
-              Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
-            K (ALLGOALS_SKIP skip
-               (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
-               DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
-                 (case prems of
-                   [] => all_tac
-                 | inv :: case_prems =>
-                     let
-                       val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
-                       val inv_thms = init @ [last];
-                       val eqs = take e inv_thms;
-                       fun is_local_var t =
-                         member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
-                        val (eqs, assms') =
-                          filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
-                        val assms = assms' @ drop e inv_thms
-                      in
-                        HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
-                        Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
-                      end)) ctxt)))])
-        end) ctxt) THEN'
-      K (prune_params_tac ctxt))
-    #> Seq.maps (fn st =>
-      CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
-  end));
+fun coinduction_tac raw_vars opt_raw_thm prems =
+  CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+    let
+      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
+      fun find_coinduct t =
+        Induct.find_coinductP ctxt t @
+        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []);
+      val raw_thm =
+        (case opt_raw_thm of
+          SOME raw_thm => raw_thm
+        | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
+      val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1;
+      val cases = Rule_Cases.get raw_thm |> fst;
+    in
+      ((Object_Logic.rulify_tac ctxt THEN'
+        Method.insert_tac ctxt prems THEN'
+        Object_Logic.atomize_prems_tac ctxt THEN'
+        DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
+          let
+            val vars = raw_vars @ map (Thm.term_of o snd) params;
+            val names_ctxt = ctxt
+              |> fold Variable.declare_names vars
+              |> fold Variable.declare_thm (raw_thm :: prems);
+            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
+            val (instT, inst) = Thm.match (thm_concl, concl);
+            val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
+            val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
+            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
+              |> map (subst_atomic_types rhoTs);
+            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
+            val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
+              |>> (fn names => Variable.variant_fixes names names_ctxt) ;
+            val eqs =
+              @{map 3} (fn name => fn T => fn (_, rhs) =>
+                HOLogic.mk_eq (Free (name, T), rhs))
+              names Ts raw_eqs;
+            val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
+              |> try (Library.foldr1 HOLogic.mk_conj)
+              |> the_default @{term True}
+              |> Ctr_Sugar_Util.list_exists_free vars
+              |> Term.map_abs_vars (Variable.revert_fixed ctxt)
+              |> fold_rev Term.absfree (names ~~ Ts)
+              |> Thm.cterm_of ctxt;
+            val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
+            val e = length eqs;
+            val p = length prems;
+          in
+            HEADGOAL (EVERY' [resolve_tac ctxt [thm],
+              EVERY' (map (fn var =>
+                resolve_tac ctxt
+                  [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
+              if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
+              else
+                REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
+                Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
+              K (ALLGOALS_SKIP skip
+                 (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
+                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
+                   (case prems of
+                     [] => all_tac
+                   | inv :: case_prems =>
+                       let
+                         val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
+                         val inv_thms = init @ [last];
+                         val eqs = take e inv_thms;
+                         fun is_local_var t =
+                           member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
+                          val (eqs, assms') =
+                            filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
+                          val assms = assms' @ drop e inv_thms
+                        in
+                          HEADGOAL (Method.insert_tac ctxt (assms @ case_prems)) THEN
+                          Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
+                        end)) ctxt)))])
+          end) ctxt) THEN'
+        K (prune_params_tac ctxt)) i) st
+      |> Seq.maps (fn st' =>
+        CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
+    end);
 
 local
 
@@ -152,8 +152,8 @@
   Theory.setup
     (Method.setup @{binding coinduction}
       (arbitrary -- Scan.option coinduct_rule >>
-        (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
-          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
+        (fn (arbitrary, opt_rule) => fn _ => fn facts =>
+          Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1)))
       "coinduction on types or predicates/sets");
 
 end;
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/functor.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -128,10 +128,11 @@
       (mapper21 $ (mapper32 $ x), mapper31 $ x);
     val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
     val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
-    fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
-      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
-        THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
-        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
+    fun prove_compositionality ctxt comp_thm =
+      Goal.prove_sorry ctxt [] [] compositionality_prop
+        (K (ALLGOALS (Method.insert_tac ctxt [@{thm fun_cong} OF [comp_thm]]
+          THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
+          THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
   in (comp_prop, prove_compositionality) end;
 
 val identity_ss =
@@ -152,9 +153,10 @@
     val rhs = HOLogic.id_const T;
     val (id_prop, identity_prop) =
       apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
-    fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
-      (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
-        Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
+    fun prove_identity ctxt id_thm =
+      Goal.prove_sorry ctxt [] [] identity_prop
+        (K (ALLGOALS (Method.insert_tac ctxt [id_thm] THEN'
+          Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
   in (id_prop, prove_identity) end;
 
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/groebner.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -970,7 +970,7 @@
      val cfs = (map swap o #multi_ideal thy evs ps)
                    (map Thm.dest_arg1 (conjuncts bod))
      val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
-    in EVERY (rev ws) THEN Method.insert_tac prems 1
+    in EVERY (rev ws) THEN Method.insert_tac ctxt prems 1
         THEN ring_tac add_ths del_ths ctxt 1
    end
   in
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -895,7 +895,9 @@
   Method.setup @{binding linarith}
     (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+        HEADGOAL
+          (Method.insert_tac ctxt
+            (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" tac;
 
diff -r c601d3c76362 -r 00b70452dc7f src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/HOL/Tools/try0.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -70,7 +70,8 @@
         ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
          (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
         I (#goal o Proof.goal)
-        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
+        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
+          #> Seq.filter_results) st
     end
   else
     NONE;
diff -r c601d3c76362 -r 00b70452dc7f src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -695,7 +695,7 @@
   end);
 
 fun prems_lin_arith_tac ctxt =
-  Method.insert_tac (Simplifier.prems_of ctxt) THEN'
+  Method.insert_tac ctxt (Simplifier.prems_of ctxt) THEN'
   simpset_lin_arith_tac ctxt;
 
 fun lin_arith_tac ctxt =
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/element.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -272,7 +272,7 @@
 local
 
 val refine_witness =
-  Proof.refine (Method.Basic (fn ctxt => EMPTY_CASES o
+  Proof.refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
     K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
@@ -283,7 +283,7 @@
     fun after_qed' thmss =
       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
-  in proof after_qed' propss #> refine_witness #> Seq.hd end;
+  in proof after_qed' propss #> refine_witness end;
 
 fun proof_local cmd goal_ctxt int after_qed propp =
   let
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -699,16 +699,16 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
-    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
 
 val _ =
   Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
-    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
 
 val _ =
   Outer_Syntax.command @{command_keyword proof} "backward proof step"
     (Scan.option Method.parse >> (fn m =>
-      (Option.map Method.report m; Toplevel.proofs (Proof.proof_results m))));
+      (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
 
 
 (* subgoal focus *)
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/method.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -4,21 +4,35 @@
 Isar proof methods.
 *)
 
+infix 1 CONTEXT_THEN_ALL_NEW;
+
+signature BASIC_METHOD =
+sig
+  type context_state = Proof.context * thm
+  type context_tactic = context_state -> context_state Seq.result Seq.seq
+  val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
+  val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
+  val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
+end;
+
 signature METHOD =
 sig
-  type method = thm list -> cases_tactic
-  val METHOD_CASES: (thm list -> cases_tactic) -> method
+  include BASIC_METHOD
+  type method = thm list -> context_tactic
+  val CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
+  val CONTEXT_TACTIC: tactic -> context_tactic
+  val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
+  val CONTEXT_METHOD: (thm list -> context_tactic) -> method
   val METHOD: (thm list -> tactic) -> method
   val fail: method
   val succeed: method
-  val insert_tac: thm list -> int -> tactic
+  val insert_tac: Proof.context -> thm list -> int -> tactic
   val insert: thm list -> method
-  val insert_facts: method
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val goal_cases_tac: Proof.context -> string list -> cases_tactic
-  val cheating: Proof.context -> bool -> method
+  val goal_cases_tac: string list -> context_tactic
+  val cheating: bool -> method
   val intro: Proof.context -> thm list -> method
   val elim: Proof.context -> thm list -> method
   val unfold: thm list -> Proof.context -> method
@@ -70,9 +84,9 @@
   val closure: bool Config.T
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val detect_closure_state: thm -> bool
-  val STATIC: (unit -> unit) -> cases_tactic
-  val RUNTIME: cases_tactic -> cases_tactic
-  val sleep: Time.time -> cases_tactic
+  val STATIC: (unit -> unit) -> context_tactic
+  val RUNTIME: context_tactic -> context_tactic
+  val sleep: Time.time -> context_tactic
   val evaluate: text -> Proof.context -> method
   type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
   val modifier: attribute -> Position.T -> modifier
@@ -92,15 +106,44 @@
 
 (** proof methods **)
 
-(* method *)
+(* tactics with proof context / cases *)
+
+type context_state = Proof.context * thm;
+type context_tactic = context_state -> context_state Seq.result Seq.seq;
+
+fun CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
+  Seq.map (Seq.Result o pair ctxt);
+
+fun CONTEXT_TACTIC tac : context_tactic =
+  fn (ctxt, st) => CONTEXT ctxt (tac st);
+
+fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
+  tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
+
+fun CONTEXT_CASES cases tac : context_tactic =
+  fn (ctxt, st) => CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
 
-type method = thm list -> cases_tactic;
+fun CONTEXT_SUBGOAL tac i : context_tactic =
+  fn (ctxt, st) =>
+    (case try Logic.nth_prem (i, Thm.prop_of st) of
+      SOME goal => tac (goal, i) (ctxt, st)
+    | NONE => Seq.empty);
 
-fun METHOD_CASES tac : method =
-  fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
+fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
+  fn (ctxt, st) =>
+    (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
+      CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
+
+
+(* type method *)
+
+type method = thm list -> context_tactic;
+
+fun CONTEXT_METHOD tac : method =
+  fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac) #> Seq.maps_results (tac facts);
 
 fun METHOD tac : method =
-  fn facts => EMPTY_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
+  fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);
@@ -108,42 +151,42 @@
 
 (* insert facts *)
 
-local
+fun insert_tac _ [] _ = all_tac
+  | insert_tac ctxt facts i =
+      EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
 
-fun cut_rule_tac rule =
-  resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
+fun insert thms =
+  CONTEXT_METHOD (fn _ => fn (ctxt, st) => st |> ALLGOALS (insert_tac ctxt thms) |> CONTEXT ctxt);
 
-in
 
-fun insert_tac [] _ = all_tac
-  | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
-
-val insert_facts = METHOD (ALLGOALS o insert_tac);
-fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
+fun SIMPLE_METHOD tac =
+  CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+    st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> CONTEXT ctxt);
 
-fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
-fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
+fun SIMPLE_METHOD'' quant tac =
+  CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+    st |> quant (insert_tac ctxt facts THEN' tac) |> CONTEXT ctxt);
+
 val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
 
-end;
-
 
 (* goals as cases *)
 
-fun goal_cases_tac ctxt case_names st =
-  let
-    val cases =
-      (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
-      |> map (rpair [] o rpair [])
-      |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
-  in Seq.single (cases, st) end;
+fun goal_cases_tac case_names : context_tactic =
+  fn (ctxt, st) =>
+    let
+      val cases =
+        (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
+        |> map (rpair [] o rpair [])
+        |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
+    in CONTEXT_CASES cases all_tac (ctxt, st) end;
 
 
 (* cheating *)
 
-fun cheating ctxt int = METHOD (fn _ => fn st =>
+fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
   if int orelse Config.get ctxt quick_and_dirty then
-    ALLGOALS (Skip_Proof.cheat_tac ctxt) st
+    CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st)
   else error "Cheating requires quick_and_dirty mode!");
 
 
@@ -164,7 +207,7 @@
 fun atomize false ctxt =
       SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
   | atomize true ctxt =
-      EMPTY_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
+      CONTEXT_TACTIC o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
 
 
 (* this -- resolve facts directly *)
@@ -262,7 +305,7 @@
 (* intros_tac -- pervasive search spanned by intro rules *)
 
 fun gen_intros_tac goals ctxt intros facts =
-  goals (insert_tac facts THEN'
+  goals (insert_tac ctxt facts THEN'
       REPEAT_ALL_NEW (resolve_tac ctxt intros))
     THEN Tactic.distinct_subgoals_tac;
 
@@ -338,7 +381,7 @@
 val standard_text = Source (Token.make_src ("standard", Position.none) []);
 val this_text = Basic this;
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
-fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
+fun sorry_text int = Basic (fn _ => cheating int);
 
 fun finish_text (NONE, immed) = Basic (finish immed)
   | finish_text (SOME txt, immed) =
@@ -424,7 +467,7 @@
   let
     val src' = map Token.init_assignable src;
     val ctxt' = Context_Position.not_really ctxt;
-    val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm));
+    val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
   in map Token.closure src' end;
 
 val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
@@ -442,39 +485,47 @@
     NONE => false
   | SOME t => Term.is_dummy_pattern t);
 
-fun STATIC test st =
-  if detect_closure_state st then (test (); Seq.single ([], st)) else Seq.empty;
+fun STATIC test : context_tactic =
+  fn (ctxt, st) =>
+    if detect_closure_state st then (test (); Seq.single (Seq.Result (ctxt, st))) else Seq.empty;
 
-fun RUNTIME (tac: cases_tactic) st =
-  if detect_closure_state st then Seq.empty else tac st;
+fun RUNTIME (tac: context_tactic) (ctxt, st) =
+  if detect_closure_state st then Seq.empty else tac (ctxt, st);
 
-fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st)));
+fun sleep t = RUNTIME (fn ctxt_st => (OS.Process.sleep t; Seq.single (Seq.Result ctxt_st)));
 
 
 (* evaluate method text *)
 
 local
 
-fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) =
-  tac st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
-
-fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) =
-  tac st |> Seq.map (pair cases);
-
 val op THEN = Seq.THEN;
 
-val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac);
+fun BYPASS_CONTEXT (tac: tactic) =
+  fn result =>
+    (case result of
+      Seq.Error _ => Seq.single result
+    | Seq.Result (ctxt, st) => tac st |> CONTEXT ctxt);
+
+val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac);
 
 fun RESTRICT_GOAL i n method =
-  BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN
+  BYPASS_CONTEXT (PRIMITIVE (Goal.restrict i n)) THEN
   method THEN
-  BYPASS_CASES (PRIMITIVE (Goal.unrestrict i));
+  BYPASS_CONTEXT (PRIMITIVE (Goal.unrestrict i));
 
 fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method;
 
-fun (method1 THEN_ALL_NEW method2) i (st: cases_state) =
-  st |> (method1 i THEN (fn st' =>
-    Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st'));
+fun (method1 THEN_ALL_NEW method2) i (result : context_state Seq.result) =
+  (case result of
+    Seq.Error _ => Seq.single result
+  | Seq.Result (_, st) =>
+      result |> method1 i
+      |> Seq.maps (fn result' =>
+          (case result' of
+            Seq.Error _ => Seq.single result'
+          | Seq.Result (_, st') =>
+              result' |> Seq.INTERVAL method2 i (i + Thm.nprems_of st' - Thm.nprems_of st))))
 
 fun COMBINATOR1 comb [meth] = comb meth
   | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
@@ -483,7 +534,7 @@
   | combinator Then_All_New =
       (fn [] => Seq.single
         | methods =>
-            preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)
+            preparation THEN (foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1))
   | combinator Orelse = Seq.FIRST
   | combinator Try = COMBINATOR1 Seq.TRY
   | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
@@ -494,15 +545,16 @@
 
 fun evaluate text ctxt =
   let
-    fun eval (Basic meth) = APPEND_CASES o meth ctxt
-      | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
+    fun eval0 m facts = Seq.single #> Seq.maps_results (m facts);
+    fun eval (Basic m) = eval0 (m ctxt)
+      | eval (Source src) = eval0 (method_cmd ctxt src ctxt)
       | eval (Combinator (_, c, txts)) =
           let
             val comb = combinator c;
             val meths = map eval txts;
           in fn facts => comb (map (fn meth => meth facts) meths) end;
     val meth = eval text;
-  in fn facts => fn st => meth facts ([], st) end;
+  in fn facts => fn ctxt_st => meth facts (Seq.Result ctxt_st) end;
 
 end;
 
@@ -680,21 +732,19 @@
   setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
   setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
     "succeed after delay (in seconds)" #>
-  setup @{binding "-"} (Scan.succeed (K insert_facts))
+  setup @{binding "-"} (Scan.succeed (K (SIMPLE_METHOD all_tac)))
     "insert current facts, nothing else" #>
-  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
-    METHOD_CASES (fn _ => fn st =>
-      let
-        val _ =
-          (case drop (Thm.nprems_of st) names of
-            [] => ()
-          | bad =>
-              if detect_closure_state st then ()
-              else
-                (* FIXME Seq.Error *)
-                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
-                  Position.here (Position.set_range (Token.range_of bad))));
-      in goal_cases_tac ctxt (map Token.content_of names) st end)))
+  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ =>
+    CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
+      (case drop (Thm.nprems_of st) names of
+        [] => NONE
+      | bad =>
+          if detect_closure_state st then NONE
+          else
+            SOME (fn () => ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+              Position.here (Position.set_range (Token.range_of bad)))))
+      |> (fn SOME msg => Seq.single (Seq.Error msg)
+           | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
     "bind cases for goals" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts" #>
@@ -723,7 +773,7 @@
       "rotate assumptions of goal" #>
   setup @{binding tactic} (parse_tactic >> (K o METHOD))
     "ML tactic as proof method" #>
-  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => EMPTY_CASES o tac))
+  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
     "ML tactic as raw proof method");
 
 
@@ -733,7 +783,10 @@
 
 end;
 
-val METHOD_CASES = Method.METHOD_CASES;
+structure Basic_Method: BASIC_METHOD = Method;
+open Basic_Method;
+
+val CONTEXT_METHOD = Method.CONTEXT_METHOD;
 val METHOD = Method.METHOD;
 val SIMPLE_METHOD = Method.SIMPLE_METHOD;
 val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -266,7 +266,7 @@
     val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
     val st = Goal.init (Thm.cterm_of ctxt thesis);
     val rule =
-      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
+      (case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
       | SOME th =>
           check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
@@ -413,9 +413,8 @@
       (SOME before_qed) after_qed
       [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> snd
-    |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
-        Goal.init (Thm.cterm_of ctxt thesis)))
-    |> Seq.hd
+    |> Proof.refine_singleton
+        (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
   end;
 
 in
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -35,8 +35,9 @@
   val has_bottom_goal: state -> bool
   val using_facts: thm list -> state -> state
   val pretty_state: state -> Pretty.T list
-  val refine: Method.text -> state -> state Seq.seq
-  val refine_end: Method.text -> state -> state Seq.seq
+  val refine: Method.text -> state -> state Seq.result Seq.seq
+  val refine_end: Method.text -> state -> state Seq.result Seq.seq
+  val refine_singleton: Method.text -> state -> state
   val refine_insert: thm list -> state -> state
   val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
@@ -90,14 +91,11 @@
   val end_block: state -> state
   val begin_notepad: context -> state
   val end_notepad: state -> context
-  val proof: Method.text option -> state -> state Seq.seq
-  val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
+  val proof: Method.text_range option -> state -> state Seq.result Seq.seq
   val defer: int -> state -> state
   val prefer: int -> state -> state
-  val apply: Method.text -> state -> state Seq.seq
-  val apply_end: Method.text -> state -> state Seq.seq
-  val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
-  val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
+  val apply: Method.text_range -> state -> state Seq.result Seq.seq
+  val apply_end: Method.text_range -> state -> state Seq.result Seq.seq
   val local_qed: Method.text_range option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
@@ -424,14 +422,13 @@
 
 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
-    |> Seq.map (fn (meth_cases, goal') =>
+    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')
-          |> Proof_Context.update_cases meth_cases;
+        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));
+          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
       in state' end));
 
 in
@@ -439,11 +436,13 @@
 fun refine text state = apply_method text (context_of state) state;
 fun refine_end text state = apply_method text (#1 (find_goal state)) state;
 
-fun refine_insert ths =
-  Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_singleton text = refine text #> Seq.the_result "";
 
-fun refine_primitive r =  (* FIXME Seq.Error!? *)
-  Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+fun refine_insert ths =
+  refine_singleton (Method.Basic (K (Method.insert ths)));
+
+fun refine_primitive r =
+  refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
 
 end;
 
@@ -924,17 +923,15 @@
 (* sub-proofs *)
 
 fun proof opt_text =
-  assert_backward
-  #> refine (the_default Method.standard_text opt_text)
-  #> Seq.map
-    (using_facts []
-      #> enter_forward
-      #> open_block
-      #> reset_goal);
-
-fun proof_results arg =
-  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
-    method_error "initial" (Method.position arg));
+  Seq.APPEND
+    (assert_backward
+      #> refine (the_default Method.standard_text (Method.text opt_text))
+      #> Seq.map_result
+        (using_facts []
+          #> enter_forward
+          #> open_block
+          #> reset_goal),
+     method_error "initial" (Method.position opt_text));
 
 fun end_proof bot (prev_pos, (opt_text, immed)) =
   let
@@ -951,8 +948,8 @@
       |> assert_current_goal true
       |> using_facts []
       |> `before_qed |-> (refine o the_default Method.succeed_text)
-      |> Seq.maps (refine finish_text)
-      |> Seq.make_results, method_error "terminal" terminal_pos)
+      |> Seq.maps_results (refine finish_text),
+      method_error "terminal" terminal_pos)
     #> Seq.maps_results (Seq.single o finished_goal finished_pos)
   end;
 
@@ -966,21 +963,18 @@
 
 fun defer i =
   assert_no_chain #>
-  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
+  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i)));
 
 fun prefer i =
   assert_no_chain #>
-  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
-
-fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
-
-fun apply_end text = assert_forward #> refine_end text;
+  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i)));
 
-fun apply_results (text, (pos, _)) =
-  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
+fun apply (text, (pos, _)) =
+  Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []),
+    method_error "" pos);
 
-fun apply_end_results (text, (pos, _)) =
-  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+fun apply_end (text, (pos, _)) =
+  Seq.APPEND (assert_forward #> refine_end text, method_error "" pos);
 
 
 
@@ -1002,10 +996,9 @@
   in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
-  refine (Method.Basic (fn ctxt => EMPTY_CASES o
+  refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
     K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
-  #> Seq.hd;
+      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
 
 in
 
@@ -1042,7 +1035,7 @@
     |> chaining ? (`the_facts #-> using_facts)
     |> reset_facts
     |> not (null vars) ? refine_terms (length goal_propss)
-    |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
   end;
 
 fun generic_qed state =
@@ -1151,7 +1144,7 @@
 local
 
 fun terminal_proof qeds initial terminal =
-  proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
+  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
   #> Seq.the_result "";
 
 in
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -4,27 +4,14 @@
 Annotations and local contexts of rules.
 *)
 
-infix 1 THEN_ALL_NEW_CASES;
-
-signature BASIC_RULE_CASES =
-sig
-  type cases
-  type cases_state = cases * thm
-  type cases_tactic = thm -> cases_state Seq.seq
-  val CASES: cases -> tactic -> cases_tactic
-  val EMPTY_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
-  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
-end
-
 signature RULE_CASES =
 sig
-  include BASIC_RULE_CASES
   datatype T = Case of
    {fixes: (binding * typ) list,
     assumes: (string * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
+  type cases = (string * T option) list
   val case_hypsN: string
   val strip_params: term -> (string * typ) list
   type info = ((string * string list) * string list) list
@@ -184,25 +171,6 @@
 
 
 
-(** tactics with cases **)
-
-type cases_state = cases * thm;
-type cases_tactic = thm -> cases_state Seq.seq;
-
-fun CASES cases tac st = Seq.map (pair cases) (tac st);
-fun EMPTY_CASES tac = CASES [] tac;
-
-fun SUBGOAL_CASES tac i st =
-  (case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i) st
-  | NONE => Seq.empty);
-
-fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
-  st |> tac1 i |> Seq.maps (fn (cases, st') =>
-    CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
-
-
-
 (** annotations and operations on rules **)
 
 (* consume facts *)
@@ -483,6 +451,3 @@
   | SOME res => res);
 
 end;
-
-structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
-open Basic_Rule_Cases;
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -429,7 +429,7 @@
     val assms =
       Proof_Context.get_fact ctxt (Facts.named "local.assms")
         handle ERROR _ => [];
-    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
+    val add_prems = Seq.hd o TRY (Method.insert_tac ctxt assms 1);
     val opt_goal' = Option.map add_prems opt_goal;
   in
     filter ctxt (all_facts_of ctxt)
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -306,10 +306,10 @@
   Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) --
   Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
     if null insts andalso null fixes
-    then quant (Method.insert_tac facts THEN' tac ctxt thms)
+    then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms)
     else
       (case thms of
-        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts fixes thm)
+        [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)
       | _ => error "Cannot have instantiations with multiple rules")));
 
 
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/simplifier.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -370,12 +370,12 @@
 fun method_setup more_mods =
   Method.setup @{binding simp}
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
-      HEADGOAL (Method.insert_tac facts THEN'
+      HEADGOAL (Method.insert_tac ctxt facts THEN'
         (CHANGED_PROP oo tac) ctxt)))
     "simplification" #>
   Method.setup @{binding simp_all}
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
-      ALLGOALS (Method.insert_tac facts) THEN
+      ALLGOALS (Method.insert_tac ctxt facts) THEN
         (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
     "simplification (all goals)";
 
diff -r c601d3c76362 -r 00b70452dc7f src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Pure/tactical.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -47,7 +47,7 @@
   val ALLGOALS: (int -> tactic) -> tactic
   val SOMEGOAL: (int -> tactic) -> tactic
   val FIRSTGOAL: (int -> tactic) -> tactic
-  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
+  val HEADGOAL: (int -> tactic) -> tactic
   val REPEAT_SOME: (int -> tactic) -> tactic
   val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   val REPEAT_FIRST: (int -> tactic) -> tactic
@@ -358,7 +358,7 @@
   following usual convention for subgoal-based tactics.*)
 fun (tac1 THEN_ALL_NEW tac2) i st =
   st |> (tac1 i THEN (fn st' =>
-    Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
+    st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));
 
 (*Repeatedly dig into any emerging subgoals.*)
 fun REPEAT_ALL_NEW tac =
diff -r c601d3c76362 -r 00b70452dc7f src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Tools/induct.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -71,23 +71,21 @@
   val rotate_tac: int -> int -> int -> tactic
   val internalize: Proof.context -> int -> thm -> thm
   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
-  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
-    thm list -> int -> cases_tactic
+  val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
   val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
-    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
-    thm list -> int -> cases_tactic
-  val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    thm list -> int -> context_tactic
+  val induct_tac: bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
-    thm list -> int -> cases_tactic
-  val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
-    thm list -> int -> cases_tactic
+    thm list -> int -> context_tactic
+  val coinduct_tac: term option list -> term option list -> thm option ->
+    thm list -> int -> context_tactic
   val gen_induct_setup: binding ->
-   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+   (bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
-    thm list -> int -> cases_tactic) ->
-   local_theory -> local_theory
+    thm list -> int -> context_tactic) -> local_theory -> local_theory
 end;
 
 functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -479,33 +477,33 @@
 
 in
 
-fun cases_tac ctxt simp insts opt_rule facts =
-  let
-    fun inst_rule r =
-      (if null insts then r
-       else
-         (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
-           |> maps (prep_inst ctxt align_left I)
-           |> infer_instantiate ctxt) r)
-      |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
-      |> pair (Rule_Cases.get r);
-
-    val (opt_rule', facts') =
-      (case (opt_rule, facts) of
-        (NONE, th :: ths) =>
-          if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
-          else (opt_rule, facts)
-      | _ => (opt_rule, facts));
-
-    val ruleq =
-      (case opt_rule' of
-        SOME r => Seq.single (inst_rule r)
-      | NONE =>
-          (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
-          |> tap (trace_rules ctxt casesN)
-          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-  in
-    fn i => fn st =>
+fun cases_tac simp insts opt_rule facts i : context_tactic =
+  fn (ctxt, st) =>
+    let
+      fun inst_rule r =
+        (if null insts then r
+         else
+           (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
+             |> maps (prep_inst ctxt align_left I)
+             |> infer_instantiate ctxt) r)
+        |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
+        |> pair (Rule_Cases.get r);
+  
+      val (opt_rule', facts') =
+        (case (opt_rule, facts) of
+          (NONE, th :: ths) =>
+            if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
+            else (opt_rule, facts)
+        | _ => (opt_rule, facts));
+  
+      val ruleq =
+        (case opt_rule' of
+          SOME r => Seq.single (inst_rule r)
+        | NONE =>
+            (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
+            |> tap (trace_rules ctxt casesN)
+            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
+    in
       ruleq
       |> Seq.maps (Rule_Cases.consume ctxt [] facts')
       |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
@@ -513,12 +511,12 @@
           val rule' = rule
             |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
         in
-          CASES (Rule_Cases.make_common ctxt
+          CONTEXT_CASES (Rule_Cases.make_common ctxt
               (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
-                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
+            ((Method.insert_tac ctxt facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
+                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) (ctxt, st)
         end)
-  end;
+    end;
 
 end;
 
@@ -741,8 +739,8 @@
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
-  SUBGOAL_CASES (fn (_, i) =>
+fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts =
+  CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
     let
       val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
       val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
@@ -773,8 +771,8 @@
           val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
           val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
         in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
-    in
-      fn st =>
+
+      fun context_tac _ _ =
         ruleq
         |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
         |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
@@ -786,7 +784,7 @@
                 val xs = nth_list arbitrary (j - 1);
                 val k = nth concls (j - 1) + more_consumes;
               in
-                Method.insert_tac (more_facts @ adefs) THEN'
+                Method.insert_tac defs_ctxt (more_facts @ adefs) THEN'
                   (if simp then
                      rotate_tac k (length adefs) THEN'
                      arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
@@ -794,17 +792,19 @@
                      arbitrary_tac defs_ctxt k xs)
                end)
             THEN' inner_atomize_tac defs_ctxt) j))
-          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+          THEN' atomize_tac defs_ctxt) i st
+        |> Seq.maps (fn st' =>
               guess_instance ctxt (internalize ctxt more_consumes rule) i st'
               |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
               |> Seq.maps (fn rule' =>
-                CASES (rule_cases ctxt rule' cases)
+                CONTEXT_CASES (rule_cases ctxt rule' cases)
                   (resolve_tac ctxt [rule'] i THEN
-                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
-      end)
-      THEN_ALL_NEW_CASES
+                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
+    in
+      (context_tac CONTEXT_THEN_ALL_NEW
         ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
-         THEN_ALL_NEW rulify_tac ctxt);
+         THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
+    end)
 
 val induct_tac = gen_induct_tac I;
 
@@ -831,15 +831,15 @@
 
 in
 
-fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
-  let
-    fun inst_rule r =
-      if null inst then `Rule_Cases.get r
-      else
-        infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
-        |> pair (Rule_Cases.get r);
-  in
-    fn st =>
+fun coinduct_tac inst taking opt_rule facts =
+  CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+    let
+      fun inst_rule r =
+        if null inst then `Rule_Cases.get r
+        else
+          infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
+          |> pair (Rule_Cases.get r);
+    in
       (case opt_rule of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
@@ -851,10 +851,10 @@
         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
-          CASES (Rule_Cases.make_common ctxt
+          CONTEXT_CASES (Rule_Cases.make_common ctxt
               (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
-  end);
+            (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
+    end);
 
 end;
 
@@ -919,8 +919,8 @@
     (Scan.lift (Args.mode no_simpN) --
       (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
         (arbitrary -- taking -- Scan.option induct_rule)) >>
-      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
-        Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
+      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn _ => fn facts =>
+        Seq.DETERM (tac (not no_simp) insts arbitrary taking opt_rule facts 1)))
     "induction on types or predicates/sets";
 
 val _ =
@@ -928,15 +928,15 @@
     (Method.local_setup @{binding cases}
       (Scan.lift (Args.mode no_simpN) --
         (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
-        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
-          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
-            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
+        (fn (no_simp, (insts, opt_rule)) => fn _ =>
+          CONTEXT_METHOD (fn facts =>
+            Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1))))
       "case analysis on types or predicates/sets" #>
     gen_induct_setup @{binding induct} induct_tac #>
      Method.local_setup @{binding coinduct}
       (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
-        (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
-          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
+        (fn ((insts, taking), opt_rule) => fn _ => fn facts =>
+          Seq.DETERM (coinduct_tac insts taking opt_rule facts 1)))
       "coinduction on types or predicates/sets");
 
 end;
diff -r c601d3c76362 -r 00b70452dc7f src/Tools/induction.ML
--- a/src/Tools/induction.ML	Sat Dec 12 18:58:06 2015 +0100
+++ b/src/Tools/induction.ML	Sun Dec 13 22:33:05 2015 +0100
@@ -7,10 +7,9 @@
 
 signature INDUCTION =
 sig
-  val induction_tac: Proof.context -> bool ->
-    (binding option * (term * bool)) option list list ->
+  val induction_tac: bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
-    thm list -> int -> cases_tactic
+    thm list -> int -> context_tactic
 end
 
 structure Induction: INDUCTION =