more general types Proof.method / context_tactic;
authorwenzelm
Sun Dec 13 21:56:15 2015 +0100 (2015-12-13)
changeset 618414d3527b94f2a
parent 61840 a3793600cb93
child 61842 00b70452dc7f
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
NEWS
src/Doc/Implementation/Isar.thy
src/HOL/Eisbach/match_method.ML
src/HOL/Filter.thy
src/HOL/Fun_Def.thy
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Partial_Function.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_lift.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_elims.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/coinduction.ML
src/HOL/Tools/functor.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/try0.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/rule_insts.ML
src/Pure/simplifier.ML
src/Pure/tactical.ML
src/Tools/induct.ML
src/Tools/induction.ML
     1.1 --- a/NEWS	Sat Dec 12 15:37:42 2015 +0100
     1.2 +++ b/NEWS	Sun Dec 13 21:56:15 2015 +0100
     1.3 @@ -626,6 +626,12 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Isar proof methods are based on a slightly more general type
     1.8 +context_tactic, which allows to change the proof context dynamically
     1.9 +(e.g. to update cases) and indicate explicit Seq.Error results. Former
    1.10 +METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
    1.11 +provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
    1.12 +
    1.13  * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
    1.14  
    1.15  * The auxiliary module Pure/display.ML has been eliminated. Its
     2.1 --- a/src/Doc/Implementation/Isar.thy	Sat Dec 12 15:37:42 2015 +0100
     2.2 +++ b/src/Doc/Implementation/Isar.thy	Sun Dec 13 21:56:15 2015 +0100
     2.3 @@ -165,12 +165,12 @@
     2.4  
     2.5  section \<open>Proof methods\<close>
     2.6  
     2.7 -text \<open>A \<open>method\<close> is a function \<open>context \<rightarrow> thm\<^sup>* \<rightarrow> goal
     2.8 -  \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*\<close> that operates on the full Isar goal
     2.9 -  configuration with context, goal facts, and tactical goal state and
    2.10 -  enumerates possible follow-up goal states, with the potential
    2.11 -  addition of named extensions of the proof context (\<^emph>\<open>cases\<close>).
    2.12 -  The latter feature is rarely used.
    2.13 +text \<open>
    2.14 +  A \<open>method\<close> is a function \<open>thm\<^sup>* \<rightarrow> context * goal \<rightarrow> (context \<times> goal)\<^sup>*\<^sup>*\<close>
    2.15 +  that operates on the full Isar goal configuration with context, goal facts,
    2.16 +  and tactical goal state and enumerates possible follow-up goal states. Under
    2.17 +  normal circumstances, the goal context remains unchanged, but it is also
    2.18 +  possible to declare named extensions of the proof context (\<^emph>\<open>cases\<close>).
    2.19  
    2.20    This means a proof method is like a structurally enhanced tactic
    2.21    (cf.\ \secref{sec:tactics}).  The well-formedness conditions for
    2.22 @@ -287,11 +287,11 @@
    2.23  text %mlref \<open>
    2.24    \begin{mldecls}
    2.25    @{index_ML_type Proof.method} \\
    2.26 -  @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\
    2.27 +  @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
    2.28    @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
    2.29    @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
    2.30    @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
    2.31 -  @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
    2.32 +  @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
    2.33    @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
    2.34    string -> theory -> theory"} \\
    2.35    \end{mldecls}
    2.36 @@ -299,9 +299,11 @@
    2.37    \<^descr> Type @{ML_type Proof.method} represents proof methods as
    2.38    abstract type.
    2.39  
    2.40 -  \<^descr> @{ML METHOD_CASES}~\<open>(fn facts => cases_tactic)\<close> wraps
    2.41 -  \<open>cases_tactic\<close> depending on goal facts as proof method with
    2.42 -  cases; the goal context is passed via method syntax.
    2.43 +  \<^descr> @{ML CONTEXT_METHOD}~\<open>(fn facts => context_tactic)\<close> wraps \<open>context_tactic\<close>
    2.44 +  depending on goal facts as a general proof method that may change the proof
    2.45 +  context dynamically. A typical operation is @{ML
    2.46 +  Proof_Context.update_cases}, which is wrapped up as combinator @{index_ML
    2.47 +  CONTEXT_CASES} for convenience.
    2.48  
    2.49    \<^descr> @{ML METHOD}~\<open>(fn facts => tactic)\<close> wraps \<open>tactic\<close> depending on goal facts as regular proof method; the goal
    2.50    context is passed via method syntax.
    2.51 @@ -315,7 +317,7 @@
    2.52    addresses a specific subgoal as simple proof method that operates on
    2.53    subgoal 1.  Goal facts are inserted into the subgoal then the \<open>tactic\<close> is applied.
    2.54  
    2.55 -  \<^descr> @{ML Method.insert_tac}~\<open>facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>.  This is convenient to reproduce
    2.56 +  \<^descr> @{ML Method.insert_tac}~\<open>ctxt facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>.  This is convenient to reproduce
    2.57    part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping
    2.58    within regular @{ML METHOD}, for example.
    2.59  
    2.60 @@ -348,7 +350,7 @@
    2.61    have "A \<and> B"
    2.62      using a and b
    2.63      ML_val \<open>@{Isar.goal}\<close>
    2.64 -    apply (tactic \<open>Method.insert_tac facts 1\<close>)
    2.65 +    apply (tactic \<open>Method.insert_tac @{context} facts 1\<close>)
    2.66      apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>)
    2.67      done
    2.68  end
     3.1 --- a/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:37:42 2015 +0100
     3.2 +++ b/src/HOL/Eisbach/match_method.ML	Sun Dec 13 21:56:15 2015 +0100
     3.3 @@ -294,9 +294,6 @@
     3.4      (text', ctxt')
     3.5    end;
     3.6  
     3.7 -fun DROP_CASES (tac: cases_tactic) : tactic =
     3.8 -  tac #> Seq.map (fn (_, st) => st);
     3.9 -
    3.10  fun prep_fact_pat ((x, args), pat) ctxt =
    3.11    let
    3.12      val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
    3.13 @@ -675,11 +672,15 @@
    3.14    in
    3.15      (case m of
    3.16        Match_Fact net =>
    3.17 -        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using st)
    3.18 -          (make_fact_matches goal_ctxt (Item_Net.retrieve net))
    3.19 +        make_fact_matches goal_ctxt (Item_Net.retrieve net)
    3.20 +        |> Seq.map (fn (text, ctxt') =>
    3.21 +          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
    3.22 +          |> Seq.filter_results |> Seq.map snd)
    3.23      | Match_Term net =>
    3.24 -        Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using st)
    3.25 -          (make_term_matches goal_ctxt (Item_Net.retrieve net))
    3.26 +        make_term_matches goal_ctxt (Item_Net.retrieve net)
    3.27 +        |> Seq.map (fn (text, ctxt') =>
    3.28 +          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
    3.29 +          |> Seq.filter_results |> Seq.map snd)
    3.30      | match_kind =>
    3.31          if Thm.no_prems st then Seq.empty
    3.32          else
    3.33 @@ -758,9 +759,9 @@
    3.34                end;
    3.35  
    3.36              fun apply_text (text, ctxt') =
    3.37 -              DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
    3.38 -              |> Seq.maps (DETERM (do_retrofit ctxt'))
    3.39 -              |> Seq.map (pair ([]: Rule_Cases.cases));
    3.40 +              Method.NO_CONTEXT_TACTIC ctxt'
    3.41 +                (Method_Closure.method_evaluate text ctxt' using) focused_goal
    3.42 +              |> Seq.maps (DETERM (do_retrofit ctxt'));
    3.43            in Seq.map apply_text texts end)
    3.44    end;
    3.45  
    3.46 @@ -770,16 +771,19 @@
    3.47        (parse_match_kind :--
    3.48          (fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
    3.49          (fn (matches, bodies) => fn ctxt =>
    3.50 -          METHOD_CASES (fn using => Method.RUNTIME (fn st =>
    3.51 +          CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
    3.52              let
    3.53 -              fun exec (pats, fixes, text) goal =
    3.54 +              fun exec (pats, fixes, text) st' =
    3.55                  let
    3.56                    val ctxt' =
    3.57                      fold Variable.declare_term fixes ctxt
    3.58                      (*FIXME Is this a good idea? We really only care about the maxidx*)
    3.59                      |> fold (fn (_, t) => Variable.declare_term t) pats;
    3.60 -                in real_match using ctxt' fixes matches text pats goal end;
    3.61 -            in Seq.flat (Seq.FIRST (map exec bodies) st) end))))
    3.62 +                in real_match using ctxt' fixes matches text pats st' end;
    3.63 +            in
    3.64 +              Seq.flat (Seq.FIRST (map exec bodies) st)
    3.65 +              |> Method.CONTEXT goal_ctxt
    3.66 +            end))))
    3.67        "structural analysis/matching on goals");
    3.68  
    3.69  end;
     4.1 --- a/src/HOL/Filter.thy	Sat Dec 12 15:37:42 2015 +0100
     4.2 +++ b/src/HOL/Filter.thy	Sun Dec 13 21:56:15 2015 +0100
     4.3 @@ -233,24 +233,23 @@
     4.4    frequently_imp_iff
     4.5  
     4.6  ML \<open>
     4.7 -  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
     4.8 -    let
     4.9 -      val mp_thms = facts RL @{thms eventually_rev_mp}
    4.10 -      val raw_elim_thm =
    4.11 -        (@{thm allI} RS @{thm always_eventually})
    4.12 -        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    4.13 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
    4.14 -      val cases_prop =
    4.15 -        Thm.prop_of
    4.16 -          (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
    4.17 -      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    4.18 -    in
    4.19 -      CASES cases (resolve_tac ctxt [raw_elim_thm] i)
    4.20 -    end)
    4.21 +  fun eventually_elim_tac facts =
    4.22 +    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
    4.23 +      let
    4.24 +        val mp_thms = facts RL @{thms eventually_rev_mp}
    4.25 +        val raw_elim_thm =
    4.26 +          (@{thm allI} RS @{thm always_eventually})
    4.27 +          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    4.28 +          |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
    4.29 +        val cases_prop =
    4.30 +          Thm.prop_of
    4.31 +            (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
    4.32 +        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    4.33 +      in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end)
    4.34  \<close>
    4.35  
    4.36  method_setup eventually_elim = \<open>
    4.37 -  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
    4.38 +  Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1))
    4.39  \<close> "elimination of eventually quantifiers"
    4.40  
    4.41  subsubsection \<open>Finer-than relation\<close>
     5.1 --- a/src/HOL/Fun_Def.thy	Sat Dec 12 15:37:42 2015 +0100
     5.2 +++ b/src/HOL/Fun_Def.thy	Sun Dec 13 21:56:15 2015 +0100
     5.3 @@ -103,7 +103,7 @@
     5.4  ML_file "Tools/Function/induction_schema.ML"
     5.5  
     5.6  method_setup induction_schema = \<open>
     5.7 -  Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac)
     5.8 +  Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
     5.9  \<close> "prove an induction principle"
    5.10  
    5.11  
     6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Dec 12 15:37:42 2015 +0100
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Dec 13 21:56:15 2015 +0100
     6.3 @@ -154,7 +154,7 @@
     6.4  fun can_apply time tac st =
     6.5    let
     6.6      val {context = ctxt, facts, goal} = Proof.goal st
     6.7 -    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
     6.8 +    val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
     6.9    in
    6.10      (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
    6.11        SOME (SOME _) => true
     7.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Dec 12 15:37:42 2015 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Dec 13 21:56:15 2015 +0100
     7.3 @@ -5,9 +5,9 @@
     7.4  
     7.5  structure NominalInduct:
     7.6  sig
     7.7 -  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     7.8 +  val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
     7.9      (string * typ) list -> (string * typ) list list -> thm list ->
    7.10 -    thm list -> int -> cases_tactic
    7.11 +    thm list -> int -> context_tactic
    7.12    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    7.13  end =
    7.14  struct
    7.15 @@ -81,7 +81,7 @@
    7.16  
    7.17  (* nominal_induct_tac *)
    7.18  
    7.19 -fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
    7.20 +fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
    7.21    let
    7.22      val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    7.23      val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
    7.24 @@ -94,8 +94,8 @@
    7.25      fun rule_cases ctxt r =
    7.26        let val r' = if simp then Induct.simplified_rule ctxt r else r
    7.27        in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
    7.28 -  in
    7.29 -    (fn i => fn st =>
    7.30 +
    7.31 +    fun context_tac _ _ =
    7.32        rules
    7.33        |> inst_mutual_rule ctxt insts avoiding
    7.34        |> Rule_Cases.consume ctxt (flat defs) facts
    7.35 @@ -108,7 +108,7 @@
    7.36                val xs = nth_list fixings (j - 1);
    7.37                val k = nth concls (j - 1) + more_consumes
    7.38              in
    7.39 -              Method.insert_tac (more_facts @ adefs) THEN'
    7.40 +              Method.insert_tac ctxt (more_facts @ adefs) THEN'
    7.41                  (if simp then
    7.42                     Induct.rotate_tac k (length adefs) THEN'
    7.43                     Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    7.44 @@ -120,13 +120,13 @@
    7.45              Induct.guess_instance ctxt
    7.46                (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
    7.47              |> Seq.maps (fn rule' =>
    7.48 -              CASES (rule_cases ctxt rule' cases)
    7.49 +              CONTEXT_CASES (rule_cases ctxt rule' cases)
    7.50                  (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
    7.51 -                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    7.52 -    THEN_ALL_NEW_CASES
    7.53 +                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
    7.54 +  in
    7.55 +    (context_tac CONTEXT_THEN_ALL_NEW
    7.56        ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
    7.57 -        else K all_tac)
    7.58 -       THEN_ALL_NEW Induct.rulify_tac ctxt)
    7.59 +        else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
    7.60    end;
    7.61  
    7.62  
    7.63 @@ -169,8 +169,8 @@
    7.64    Scan.lift (Args.mode Induct.no_simpN) --
    7.65    (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    7.66      avoiding -- fixing -- rule_spec) >>
    7.67 -  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
    7.68 -    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
    7.69 +  (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
    7.70 +    (nominal_induct_tac (not no_simp) x y z w facts 1));
    7.71  
    7.72  end;
    7.73  
     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 12 15:37:42 2015 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Dec 13 21:56:15 2015 +0100
     8.3 @@ -372,11 +372,10 @@
     8.4            |> snd
     8.5          end)
     8.6        [goals] |>
     8.7 -    Proof.apply (Method.Basic (fn ctxt => fn _ =>
     8.8 -      EMPTY_CASES
     8.9 +    Proof.refine_singleton (Method.Basic (fn ctxt => fn _ =>
    8.10 +      Method.CONTEXT_TACTIC
    8.11         (rewrite_goals_tac ctxt defs_thms THEN
    8.12 -        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
    8.13 -    Seq.hd
    8.14 +        compose_tac ctxt (false, rule, length rule_prems) 1)))
    8.15    end;
    8.16  
    8.17  in
     9.1 --- a/src/HOL/Partial_Function.thy	Sat Dec 12 15:37:42 2015 +0100
     9.2 +++ b/src/HOL/Partial_Function.thy	Sun Dec 13 21:56:15 2015 +0100
     9.3 @@ -443,7 +443,7 @@
     9.4  
     9.5  declaration \<open>Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
     9.6    @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
     9.7 -  (SOME @{thm fixp_induct_tailrec[where c=undefined]})\<close>
     9.8 +  (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
     9.9  
    9.10  declaration \<open>Partial_Function.init "option" @{term option.fixp_fun}
    9.11    @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
    10.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Dec 12 15:37:42 2015 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Dec 13 21:56:15 2015 +0100
    10.3 @@ -1706,8 +1706,7 @@
    10.4        (lthy
    10.5         |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
    10.6           (map (single o rpair []) goals @ nontriv_wit_goals)
    10.7 -       |> Proof.refine (Method.primitive_text (K I))
    10.8 -       |> Seq.hd)
    10.9 +       |> Proof.refine_singleton (Method.primitive_text (K I)))
   10.10    end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
   10.11      NONE Binding.empty Binding.empty [] raw_csts;
   10.12  
    11.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Dec 12 15:37:42 2015 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Dec 13 21:56:15 2015 +0100
    11.3 @@ -319,7 +319,7 @@
    11.4        unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
    11.5        unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
    11.6        EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
    11.7 -        Method.insert_tac inserts, REPEAT_DETERM o dtac ctxt meta_spec,
    11.8 +        Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
    11.9          REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
   11.10          if live = 1 then K all_tac
   11.11          else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
    12.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Dec 12 15:37:42 2015 +0100
    12.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Dec 13 21:56:15 2015 +0100
    12.3 @@ -1579,8 +1579,7 @@
    12.4  val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
    12.5    lthy
    12.6    |> Proof.theorem NONE after_qed goalss
    12.7 -  |> Proof.refine (Method.primitive_text (K I))
    12.8 -  |> Seq.hd) ooo primcorec_ursive_cmd false;
    12.9 +  |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
   12.10  
   12.11  val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
   12.12      lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
    13.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 12 15:37:42 2015 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Dec 13 21:56:15 2015 +0100
    13.3 @@ -54,7 +54,7 @@
    13.4    assume_tac ctxt;
    13.5  
    13.6  fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
    13.7 -  HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
    13.8 +  HEADGOAL (Method.insert_tac ctxt exhaust_discs THEN' clean_blast_tac ctxt);
    13.9  
   13.10  fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   13.11    let val ks = 1 upto n in
    14.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Dec 12 15:37:42 2015 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sun Dec 13 21:56:15 2015 +0100
    14.3 @@ -1082,7 +1082,7 @@
    14.4  fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
    14.5    let val n = length in_rels;
    14.6    in
    14.7 -    Method.insert_tac CIHs 1 THEN
    14.8 +    Method.insert_tac ctxt CIHs 1 THEN
    14.9      unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
   14.10      REPEAT_DETERM (etac ctxt exE 1) THEN
   14.11      CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
    15.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Dec 12 15:37:42 2015 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Dec 13 21:56:15 2015 +0100
    15.3 @@ -356,7 +356,7 @@
    15.4    let
    15.5      val n = length card_of_min_algs;
    15.6    in
    15.7 -    EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
    15.8 +    EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
    15.9        REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
   15.10        rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
   15.11        rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
    16.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Sat Dec 12 15:37:42 2015 +0100
    16.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Dec 13 21:56:15 2015 +0100
    16.3 @@ -345,10 +345,9 @@
    16.4    (fn (goals, after_qed, definitions, lthy) =>
    16.5      lthy
    16.6      |> Proof.theorem NONE after_qed (map (single o rpair []) goals)
    16.7 -    |> Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
    16.8 -    |> Seq.hd
    16.9 -    |> Proof.refine (Method.primitive_text (K I))
   16.10 -    |> Seq.hd) oo
   16.11 +    |> Proof.refine_singleton
   16.12 +        (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
   16.13 +    |> Proof.refine_singleton (Method.primitive_text (K I))) oo
   16.14    prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME));
   16.15  
   16.16  fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs =
    17.1 --- a/src/HOL/Tools/Function/function.ML	Sat Dec 12 15:37:42 2015 +0100
    17.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Dec 13 21:56:15 2015 +0100
    17.3 @@ -171,7 +171,7 @@
    17.4    in
    17.5      lthy'
    17.6      |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
    17.7 -    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
    17.8 +    |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
    17.9    end
   17.10  
   17.11  val function =
    18.1 --- a/src/HOL/Tools/Function/function_elims.ML	Sat Dec 12 15:37:42 2015 +0100
    18.2 +++ b/src/HOL/Tools/Function/function_elims.ML	Sun Dec 13 21:56:15 2015 +0100
    18.3 @@ -121,7 +121,7 @@
    18.4  
    18.5          fun prep_subgoal_tac i =
    18.6            REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
    18.7 -          THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
    18.8 +          THEN Method.insert_tac ctxt (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
    18.9            THEN propagate_tac ctxt i
   18.10            THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
   18.11            THEN bool_subst_tac ctxt i;
    19.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Dec 12 15:37:42 2015 +0100
    19.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Dec 13 21:56:15 2015 +0100
    19.3 @@ -345,7 +345,7 @@
    19.4  
    19.5  fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
    19.6    (* FIXME proper use of facts!? *)
    19.7 -  (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
    19.8 +  (ALLGOALS (Method.insert_tac ctxt facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
    19.9    let
   19.10      val (ctxt', _, cases, concl) = dest_hhf ctxt t
   19.11      val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
    20.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sat Dec 12 15:37:42 2015 +0100
    20.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sun Dec 13 21:56:15 2015 +0100
    20.3 @@ -62,8 +62,6 @@
    20.4  
    20.5  (*** Automated monotonicity proofs ***)
    20.6  
    20.7 -fun strip_cases ctac = ctac #> Seq.map snd;
    20.8 -
    20.9  (*rewrite conclusion with k-th assumtion*)
   20.10  fun rewrite_with_asm_tac ctxt k =
   20.11    Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   20.12 @@ -95,7 +93,7 @@
   20.13         | SOME (arg, conv) =>
   20.14             let open Conv in
   20.15                if Term.is_open arg then no_tac
   20.16 -              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
   20.17 +              else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
   20.18                  THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
   20.19                  THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
   20.20                  THEN_ALL_NEW (CONVERSION
    21.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Dec 12 15:37:42 2015 +0100
    21.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Dec 13 21:56:15 2015 +0100
    21.3 @@ -407,7 +407,7 @@
    21.4        by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
    21.5  
    21.6      fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
    21.7 -        (Method.insert_tac wits THEN' 
    21.8 +        (Method.insert_tac ctxt wits THEN' 
    21.9           eq_onp_to_top_tac ctxt THEN' (* normalize *)
   21.10           rtac ctxt unfold_lift_sel_rsp THEN'
   21.11           case_tac exhaust_rule ctxt THEN_ALL_NEW (
   21.12 @@ -559,7 +559,7 @@
   21.13          val TFrees = Term.add_tfreesT qty []
   21.14  
   21.15          fun non_empty_typedef_tac non_empty_pred ctxt i =
   21.16 -          (Method.insert_tac [non_empty_pred] THEN' 
   21.17 +          (Method.insert_tac ctxt [non_empty_pred] THEN' 
   21.18              SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
   21.19          val uTname = unique_Tname (rty, qty)
   21.20          val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
    22.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Dec 12 15:37:42 2015 +0100
    22.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sun Dec 13 21:56:15 2015 +0100
    22.3 @@ -272,7 +272,7 @@
    22.4  
    22.5  fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
    22.6    let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
    22.7 -    HEADGOAL (Method.insert_tac nonschem_facts THEN'
    22.8 +    HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
    22.9        CHANGED_PROP o metis_tac (these override_type_encs)
   22.10          (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   22.11    end
    23.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 12 15:37:42 2015 +0100
    23.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Dec 13 21:56:15 2015 +0100
    23.3 @@ -870,7 +870,7 @@
    23.4      val simpset_ctxt =
    23.5        put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
    23.6    in
    23.7 -    Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}))
    23.8 +    Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}))
    23.9      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
   23.10      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   23.11      THEN_ALL_NEW simp_tac simpset_ctxt
    24.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Dec 12 15:37:42 2015 +0100
    24.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Dec 13 21:56:15 2015 +0100
    24.3 @@ -133,7 +133,7 @@
    24.4  fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
    24.5  
    24.6  fun prop_tac ctxt prems =
    24.7 -  Method.insert_tac prems
    24.8 +  Method.insert_tac ctxt prems
    24.9    THEN' SUBGOAL (fn (prop, i) =>
   24.10      if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
   24.11      else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
   24.12 @@ -324,7 +324,7 @@
   24.13    by fast+}
   24.14  
   24.15  fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
   24.16 -  Method.insert_tac thms
   24.17 +  Method.insert_tac ctxt thms
   24.18    THEN' (Classical.fast_tac ctxt'
   24.19      ORELSE' dresolve_tac ctxt cong_dest_rules
   24.20      THEN' Classical.fast_tac ctxt'))
   24.21 @@ -615,7 +615,7 @@
   24.22  (* theory lemmas *)
   24.23  
   24.24  fun arith_th_lemma_tac ctxt prems =
   24.25 -  Method.insert_tac prems
   24.26 +  Method.insert_tac ctxt prems
   24.27    THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
   24.28    THEN' Arith_Data.arith_tac ctxt
   24.29  
    25.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Dec 12 15:37:42 2015 +0100
    25.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun Dec 13 21:56:15 2015 +0100
    25.3 @@ -114,7 +114,7 @@
    25.4    end
    25.5  
    25.6  fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
    25.7 -  Method.insert_tac local_facts THEN'
    25.8 +  Method.insert_tac ctxt local_facts THEN'
    25.9    (case meth of
   25.10      Metis_Method (type_enc_opt, lam_trans_opt) =>
   25.11      let
   25.12 @@ -131,7 +131,7 @@
   25.13    | Simp_Size_Method =>
   25.14      Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
   25.15    | _ =>
   25.16 -    Method.insert_tac global_facts THEN'
   25.17 +    Method.insert_tac ctxt global_facts THEN'
   25.18      (case meth of
   25.19        SATx_Method => SAT.satx_tac ctxt
   25.20      | Blast_Method => blast_tac ctxt
    26.1 --- a/src/HOL/Tools/arith_data.ML	Sat Dec 12 15:37:42 2015 +0100
    26.2 +++ b/src/HOL/Tools/arith_data.ML	Sun Dec 13 21:56:15 2015 +0100
    26.3 @@ -48,8 +48,8 @@
    26.4        (Scan.succeed (fn ctxt =>
    26.5          METHOD (fn facts =>
    26.6            HEADGOAL
    26.7 -          (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    26.8 -            THEN' arith_tac ctxt))))
    26.9 +            (Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
   26.10 +              THEN' arith_tac ctxt))))
   26.11        "various arithmetic decision procedures");
   26.12  
   26.13  
    27.1 --- a/src/HOL/Tools/coinduction.ML	Sat Dec 12 15:37:42 2015 +0100
    27.2 +++ b/src/HOL/Tools/coinduction.ML	Sun Dec 13 21:56:15 2015 +0100
    27.3 @@ -8,7 +8,7 @@
    27.4  
    27.5  signature COINDUCTION =
    27.6  sig
    27.7 -  val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
    27.8 +  val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic
    27.9  end;
   27.10  
   27.11  structure Coinduction : COINDUCTION =
   27.12 @@ -37,85 +37,85 @@
   27.13      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
   27.14    end;
   27.15  
   27.16 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _) =>
   27.17 -  let
   27.18 -    val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
   27.19 -    fun find_coinduct t =
   27.20 -      Induct.find_coinductP ctxt t @
   27.21 -      (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
   27.22 -    val raw_thm =
   27.23 -      (case opt_raw_thm of
   27.24 -        SOME raw_thm => raw_thm
   27.25 -      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
   27.26 -    val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
   27.27 -    val cases = Rule_Cases.get raw_thm |> fst
   27.28 -  in
   27.29 -    HEADGOAL (
   27.30 -      Object_Logic.rulify_tac ctxt THEN'
   27.31 -      Method.insert_tac prems THEN'
   27.32 -      Object_Logic.atomize_prems_tac ctxt THEN'
   27.33 -      DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
   27.34 -        let
   27.35 -          val vars = raw_vars @ map (Thm.term_of o snd) params;
   27.36 -          val names_ctxt = ctxt
   27.37 -            |> fold Variable.declare_names vars
   27.38 -            |> fold Variable.declare_thm (raw_thm :: prems);
   27.39 -          val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
   27.40 -          val (instT, inst) = Thm.match (thm_concl, concl);
   27.41 -          val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
   27.42 -          val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
   27.43 -          val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
   27.44 -            |> map (subst_atomic_types rhoTs);
   27.45 -          val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
   27.46 -          val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
   27.47 -            |>> (fn names => Variable.variant_fixes names names_ctxt) ;
   27.48 -          val eqs =
   27.49 -            @{map 3} (fn name => fn T => fn (_, rhs) =>
   27.50 -              HOLogic.mk_eq (Free (name, T), rhs))
   27.51 -            names Ts raw_eqs;
   27.52 -          val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
   27.53 -            |> try (Library.foldr1 HOLogic.mk_conj)
   27.54 -            |> the_default @{term True}
   27.55 -            |> Ctr_Sugar_Util.list_exists_free vars
   27.56 -            |> Term.map_abs_vars (Variable.revert_fixed ctxt)
   27.57 -            |> fold_rev Term.absfree (names ~~ Ts)
   27.58 -            |> Thm.cterm_of ctxt;
   27.59 -          val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
   27.60 -          val e = length eqs;
   27.61 -          val p = length prems;
   27.62 -        in
   27.63 -          HEADGOAL (EVERY' [resolve_tac ctxt [thm],
   27.64 -            EVERY' (map (fn var =>
   27.65 -              resolve_tac ctxt
   27.66 -                [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
   27.67 -            if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
   27.68 -            else
   27.69 -              REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
   27.70 -              Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
   27.71 -            K (ALLGOALS_SKIP skip
   27.72 -               (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
   27.73 -               DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
   27.74 -                 (case prems of
   27.75 -                   [] => all_tac
   27.76 -                 | inv :: case_prems =>
   27.77 -                     let
   27.78 -                       val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
   27.79 -                       val inv_thms = init @ [last];
   27.80 -                       val eqs = take e inv_thms;
   27.81 -                       fun is_local_var t =
   27.82 -                         member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
   27.83 -                        val (eqs, assms') =
   27.84 -                          filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
   27.85 -                        val assms = assms' @ drop e inv_thms
   27.86 -                      in
   27.87 -                        HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
   27.88 -                        Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
   27.89 -                      end)) ctxt)))])
   27.90 -        end) ctxt) THEN'
   27.91 -      K (prune_params_tac ctxt))
   27.92 -    #> Seq.maps (fn st =>
   27.93 -      CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
   27.94 -  end));
   27.95 +fun coinduction_tac raw_vars opt_raw_thm prems =
   27.96 +  CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
   27.97 +    let
   27.98 +      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
   27.99 +      fun find_coinduct t =
  27.100 +        Induct.find_coinductP ctxt t @
  27.101 +        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []);
  27.102 +      val raw_thm =
  27.103 +        (case opt_raw_thm of
  27.104 +          SOME raw_thm => raw_thm
  27.105 +        | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
  27.106 +      val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1;
  27.107 +      val cases = Rule_Cases.get raw_thm |> fst;
  27.108 +    in
  27.109 +      ((Object_Logic.rulify_tac ctxt THEN'
  27.110 +        Method.insert_tac ctxt prems THEN'
  27.111 +        Object_Logic.atomize_prems_tac ctxt THEN'
  27.112 +        DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
  27.113 +          let
  27.114 +            val vars = raw_vars @ map (Thm.term_of o snd) params;
  27.115 +            val names_ctxt = ctxt
  27.116 +              |> fold Variable.declare_names vars
  27.117 +              |> fold Variable.declare_thm (raw_thm :: prems);
  27.118 +            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
  27.119 +            val (instT, inst) = Thm.match (thm_concl, concl);
  27.120 +            val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
  27.121 +            val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
  27.122 +            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
  27.123 +              |> map (subst_atomic_types rhoTs);
  27.124 +            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
  27.125 +            val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
  27.126 +              |>> (fn names => Variable.variant_fixes names names_ctxt) ;
  27.127 +            val eqs =
  27.128 +              @{map 3} (fn name => fn T => fn (_, rhs) =>
  27.129 +                HOLogic.mk_eq (Free (name, T), rhs))
  27.130 +              names Ts raw_eqs;
  27.131 +            val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
  27.132 +              |> try (Library.foldr1 HOLogic.mk_conj)
  27.133 +              |> the_default @{term True}
  27.134 +              |> Ctr_Sugar_Util.list_exists_free vars
  27.135 +              |> Term.map_abs_vars (Variable.revert_fixed ctxt)
  27.136 +              |> fold_rev Term.absfree (names ~~ Ts)
  27.137 +              |> Thm.cterm_of ctxt;
  27.138 +            val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
  27.139 +            val e = length eqs;
  27.140 +            val p = length prems;
  27.141 +          in
  27.142 +            HEADGOAL (EVERY' [resolve_tac ctxt [thm],
  27.143 +              EVERY' (map (fn var =>
  27.144 +                resolve_tac ctxt
  27.145 +                  [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
  27.146 +              if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
  27.147 +              else
  27.148 +                REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
  27.149 +                Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
  27.150 +              K (ALLGOALS_SKIP skip
  27.151 +                 (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
  27.152 +                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
  27.153 +                   (case prems of
  27.154 +                     [] => all_tac
  27.155 +                   | inv :: case_prems =>
  27.156 +                       let
  27.157 +                         val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
  27.158 +                         val inv_thms = init @ [last];
  27.159 +                         val eqs = take e inv_thms;
  27.160 +                         fun is_local_var t =
  27.161 +                           member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
  27.162 +                          val (eqs, assms') =
  27.163 +                            filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
  27.164 +                          val assms = assms' @ drop e inv_thms
  27.165 +                        in
  27.166 +                          HEADGOAL (Method.insert_tac ctxt (assms @ case_prems)) THEN
  27.167 +                          Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
  27.168 +                        end)) ctxt)))])
  27.169 +          end) ctxt) THEN'
  27.170 +        K (prune_params_tac ctxt)) i) st
  27.171 +      |> Seq.maps (fn st' =>
  27.172 +        CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
  27.173 +    end);
  27.174  
  27.175  local
  27.176  
  27.177 @@ -152,8 +152,8 @@
  27.178    Theory.setup
  27.179      (Method.setup @{binding coinduction}
  27.180        (arbitrary -- Scan.option coinduct_rule >>
  27.181 -        (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
  27.182 -          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
  27.183 +        (fn (arbitrary, opt_rule) => fn _ => fn facts =>
  27.184 +          Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1)))
  27.185        "coinduction on types or predicates/sets");
  27.186  
  27.187  end;
    28.1 --- a/src/HOL/Tools/functor.ML	Sat Dec 12 15:37:42 2015 +0100
    28.2 +++ b/src/HOL/Tools/functor.ML	Sun Dec 13 21:56:15 2015 +0100
    28.3 @@ -128,10 +128,11 @@
    28.4        (mapper21 $ (mapper32 $ x), mapper31 $ x);
    28.5      val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
    28.6      val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
    28.7 -    fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
    28.8 -      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
    28.9 -        THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
   28.10 -        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
   28.11 +    fun prove_compositionality ctxt comp_thm =
   28.12 +      Goal.prove_sorry ctxt [] [] compositionality_prop
   28.13 +        (K (ALLGOALS (Method.insert_tac ctxt [@{thm fun_cong} OF [comp_thm]]
   28.14 +          THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
   28.15 +          THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
   28.16    in (comp_prop, prove_compositionality) end;
   28.17  
   28.18  val identity_ss =
   28.19 @@ -152,9 +153,10 @@
   28.20      val rhs = HOLogic.id_const T;
   28.21      val (id_prop, identity_prop) =
   28.22        apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
   28.23 -    fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
   28.24 -      (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
   28.25 -        Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
   28.26 +    fun prove_identity ctxt id_thm =
   28.27 +      Goal.prove_sorry ctxt [] [] identity_prop
   28.28 +        (K (ALLGOALS (Method.insert_tac ctxt [id_thm] THEN'
   28.29 +          Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
   28.30    in (id_prop, prove_identity) end;
   28.31  
   28.32  
    29.1 --- a/src/HOL/Tools/groebner.ML	Sat Dec 12 15:37:42 2015 +0100
    29.2 +++ b/src/HOL/Tools/groebner.ML	Sun Dec 13 21:56:15 2015 +0100
    29.3 @@ -970,7 +970,7 @@
    29.4       val cfs = (map swap o #multi_ideal thy evs ps)
    29.5                     (map Thm.dest_arg1 (conjuncts bod))
    29.6       val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
    29.7 -    in EVERY (rev ws) THEN Method.insert_tac prems 1
    29.8 +    in EVERY (rev ws) THEN Method.insert_tac ctxt prems 1
    29.9          THEN ring_tac add_ths del_ths ctxt 1
   29.10     end
   29.11    in
    30.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Dec 12 15:37:42 2015 +0100
    30.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Dec 13 21:56:15 2015 +0100
    30.3 @@ -895,7 +895,9 @@
    30.4    Method.setup @{binding linarith}
    30.5      (Scan.succeed (fn ctxt =>
    30.6        METHOD (fn facts =>
    30.7 -        HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    30.8 +        HEADGOAL
    30.9 +          (Method.insert_tac ctxt
   30.10 +            (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
   30.11            THEN' tac ctxt)))) "linear arithmetic" #>
   30.12    Arith_Data.add_tactic "linear arithmetic" tac;
   30.13  
    31.1 --- a/src/HOL/Tools/try0.ML	Sat Dec 12 15:37:42 2015 +0100
    31.2 +++ b/src/HOL/Tools/try0.ML	Sun Dec 13 21:56:15 2015 +0100
    31.3 @@ -70,7 +70,8 @@
    31.4          ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
    31.5           (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
    31.6          I (#goal o Proof.goal)
    31.7 -        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
    31.8 +        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
    31.9 +          #> Seq.filter_results) st
   31.10      end
   31.11    else
   31.12      NONE;
    32.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat Dec 12 15:37:42 2015 +0100
    32.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Dec 13 21:56:15 2015 +0100
    32.3 @@ -695,7 +695,7 @@
    32.4    end);
    32.5  
    32.6  fun prems_lin_arith_tac ctxt =
    32.7 -  Method.insert_tac (Simplifier.prems_of ctxt) THEN'
    32.8 +  Method.insert_tac ctxt (Simplifier.prems_of ctxt) THEN'
    32.9    simpset_lin_arith_tac ctxt;
   32.10  
   32.11  fun lin_arith_tac ctxt =
    33.1 --- a/src/Pure/Isar/element.ML	Sat Dec 12 15:37:42 2015 +0100
    33.2 +++ b/src/Pure/Isar/element.ML	Sun Dec 13 21:56:15 2015 +0100
    33.3 @@ -272,7 +272,7 @@
    33.4  local
    33.5  
    33.6  val refine_witness =
    33.7 -  Proof.refine (Method.Basic (fn ctxt => EMPTY_CASES o
    33.8 +  Proof.refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
    33.9      K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
   33.10  
   33.11  fun gen_witness_proof proof after_qed wit_propss eq_props =
   33.12 @@ -283,7 +283,7 @@
   33.13      fun after_qed' thmss =
   33.14        let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
   33.15        in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   33.16 -  in proof after_qed' propss #> refine_witness #> Seq.hd end;
   33.17 +  in proof after_qed' propss #> refine_witness end;
   33.18  
   33.19  fun proof_local cmd goal_ctxt int after_qed propp =
   33.20    let
    34.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 12 15:37:42 2015 +0100
    34.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Dec 13 21:56:15 2015 +0100
    34.3 @@ -699,16 +699,16 @@
    34.4  
    34.5  val _ =
    34.6    Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
    34.7 -    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
    34.8 +    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
    34.9  
   34.10  val _ =
   34.11    Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
   34.12 -    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
   34.13 +    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
   34.14  
   34.15  val _ =
   34.16    Outer_Syntax.command @{command_keyword proof} "backward proof step"
   34.17      (Scan.option Method.parse >> (fn m =>
   34.18 -      (Option.map Method.report m; Toplevel.proofs (Proof.proof_results m))));
   34.19 +      (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
   34.20  
   34.21  
   34.22  (* subgoal focus *)
    35.1 --- a/src/Pure/Isar/method.ML	Sat Dec 12 15:37:42 2015 +0100
    35.2 +++ b/src/Pure/Isar/method.ML	Sun Dec 13 21:56:15 2015 +0100
    35.3 @@ -4,34 +4,35 @@
    35.4  Isar proof methods.
    35.5  *)
    35.6  
    35.7 -infix 1 THEN_ALL_NEW_CASES;
    35.8 +infix 1 CONTEXT_THEN_ALL_NEW;
    35.9  
   35.10  signature BASIC_METHOD =
   35.11  sig
   35.12 -  type cases_state = Rule_Cases.cases * thm
   35.13 -  type cases_tactic = thm -> cases_state Seq.seq
   35.14 -  val CASES: Rule_Cases.cases -> tactic -> cases_tactic
   35.15 -  val EMPTY_CASES: tactic -> cases_tactic
   35.16 -  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
   35.17 -  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
   35.18 +  type context_state = Proof.context * thm
   35.19 +  type context_tactic = context_state -> context_state Seq.result Seq.seq
   35.20 +  val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
   35.21 +  val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
   35.22 +  val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
   35.23  end;
   35.24  
   35.25  signature METHOD =
   35.26  sig
   35.27    include BASIC_METHOD
   35.28 -  type method = thm list -> cases_tactic
   35.29 -  val METHOD_CASES: (thm list -> cases_tactic) -> method
   35.30 +  type method = thm list -> context_tactic
   35.31 +  val CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
   35.32 +  val CONTEXT_TACTIC: tactic -> context_tactic
   35.33 +  val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
   35.34 +  val CONTEXT_METHOD: (thm list -> context_tactic) -> method
   35.35    val METHOD: (thm list -> tactic) -> method
   35.36    val fail: method
   35.37    val succeed: method
   35.38 -  val insert_tac: thm list -> int -> tactic
   35.39 +  val insert_tac: Proof.context -> thm list -> int -> tactic
   35.40    val insert: thm list -> method
   35.41 -  val insert_facts: method
   35.42    val SIMPLE_METHOD: tactic -> method
   35.43    val SIMPLE_METHOD': (int -> tactic) -> method
   35.44    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
   35.45 -  val goal_cases_tac: Proof.context -> string list -> cases_tactic
   35.46 -  val cheating: Proof.context -> bool -> method
   35.47 +  val goal_cases_tac: string list -> context_tactic
   35.48 +  val cheating: bool -> method
   35.49    val intro: Proof.context -> thm list -> method
   35.50    val elim: Proof.context -> thm list -> method
   35.51    val unfold: thm list -> Proof.context -> method
   35.52 @@ -83,9 +84,9 @@
   35.53    val closure: bool Config.T
   35.54    val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   35.55    val detect_closure_state: thm -> bool
   35.56 -  val STATIC: (unit -> unit) -> cases_tactic
   35.57 -  val RUNTIME: cases_tactic -> cases_tactic
   35.58 -  val sleep: Time.time -> cases_tactic
   35.59 +  val STATIC: (unit -> unit) -> context_tactic
   35.60 +  val RUNTIME: context_tactic -> context_tactic
   35.61 +  val sleep: Time.time -> context_tactic
   35.62    val evaluate: text -> Proof.context -> method
   35.63    type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
   35.64    val modifier: attribute -> Position.T -> modifier
   35.65 @@ -105,33 +106,44 @@
   35.66  
   35.67  (** proof methods **)
   35.68  
   35.69 -(* tactics with cases *)
   35.70 +(* tactics with proof context / cases *)
   35.71 +
   35.72 +type context_state = Proof.context * thm;
   35.73 +type context_tactic = context_state -> context_state Seq.result Seq.seq;
   35.74  
   35.75 -type cases_state = Rule_Cases.cases * thm;
   35.76 -type cases_tactic = thm -> cases_state Seq.seq;
   35.77 +fun CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
   35.78 +  Seq.map (Seq.Result o pair ctxt);
   35.79  
   35.80 -fun CASES cases tac st = Seq.map (pair cases) (tac st);
   35.81 -fun EMPTY_CASES tac = CASES [] tac;
   35.82 +fun CONTEXT_TACTIC tac : context_tactic =
   35.83 +  fn (ctxt, st) => CONTEXT ctxt (tac st);
   35.84 +
   35.85 +fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
   35.86 +  tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
   35.87  
   35.88 -fun SUBGOAL_CASES tac i st =
   35.89 -  (case try Logic.nth_prem (i, Thm.prop_of st) of
   35.90 -    SOME goal => tac (goal, i) st
   35.91 -  | NONE => Seq.empty);
   35.92 +fun CONTEXT_CASES cases tac : context_tactic =
   35.93 +  fn (ctxt, st) => CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
   35.94  
   35.95 -fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   35.96 -  st |> tac1 i |> Seq.maps (fn (cases, st') =>
   35.97 -    CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
   35.98 +fun CONTEXT_SUBGOAL tac i : context_tactic =
   35.99 +  fn (ctxt, st) =>
  35.100 +    (case try Logic.nth_prem (i, Thm.prop_of st) of
  35.101 +      SOME goal => tac (goal, i) (ctxt, st)
  35.102 +    | NONE => Seq.empty);
  35.103 +
  35.104 +fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
  35.105 +  fn (ctxt, st) =>
  35.106 +    (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
  35.107 +      CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
  35.108  
  35.109  
  35.110  (* type method *)
  35.111  
  35.112 -type method = thm list -> cases_tactic;
  35.113 +type method = thm list -> context_tactic;
  35.114  
  35.115 -fun METHOD_CASES tac : method =
  35.116 -  fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
  35.117 +fun CONTEXT_METHOD tac : method =
  35.118 +  fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac) #> Seq.maps_results (tac facts);
  35.119  
  35.120  fun METHOD tac : method =
  35.121 -  fn facts => EMPTY_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
  35.122 +  fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac THEN tac facts);
  35.123  
  35.124  val fail = METHOD (K no_tac);
  35.125  val succeed = METHOD (K all_tac);
  35.126 @@ -139,42 +151,42 @@
  35.127  
  35.128  (* insert facts *)
  35.129  
  35.130 -local
  35.131 +fun insert_tac _ [] _ = all_tac
  35.132 +  | insert_tac ctxt facts i =
  35.133 +      EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
  35.134  
  35.135 -fun cut_rule_tac rule =
  35.136 -  resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
  35.137 +fun insert thms =
  35.138 +  CONTEXT_METHOD (fn _ => fn (ctxt, st) => st |> ALLGOALS (insert_tac ctxt thms) |> CONTEXT ctxt);
  35.139  
  35.140 -in
  35.141  
  35.142 -fun insert_tac [] _ = all_tac
  35.143 -  | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
  35.144 -
  35.145 -val insert_facts = METHOD (ALLGOALS o insert_tac);
  35.146 -fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
  35.147 +fun SIMPLE_METHOD tac =
  35.148 +  CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
  35.149 +    st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> CONTEXT ctxt);
  35.150  
  35.151 -fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
  35.152 -fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
  35.153 +fun SIMPLE_METHOD'' quant tac =
  35.154 +  CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
  35.155 +    st |> quant (insert_tac ctxt facts THEN' tac) |> CONTEXT ctxt);
  35.156 +
  35.157  val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
  35.158  
  35.159 -end;
  35.160 -
  35.161  
  35.162  (* goals as cases *)
  35.163  
  35.164 -fun goal_cases_tac ctxt case_names st =
  35.165 -  let
  35.166 -    val cases =
  35.167 -      (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
  35.168 -      |> map (rpair [] o rpair [])
  35.169 -      |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
  35.170 -  in Seq.single (cases, st) end;
  35.171 +fun goal_cases_tac case_names : context_tactic =
  35.172 +  fn (ctxt, st) =>
  35.173 +    let
  35.174 +      val cases =
  35.175 +        (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
  35.176 +        |> map (rpair [] o rpair [])
  35.177 +        |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
  35.178 +    in CONTEXT_CASES cases all_tac (ctxt, st) end;
  35.179  
  35.180  
  35.181  (* cheating *)
  35.182  
  35.183 -fun cheating ctxt int = METHOD (fn _ => fn st =>
  35.184 +fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
  35.185    if int orelse Config.get ctxt quick_and_dirty then
  35.186 -    ALLGOALS (Skip_Proof.cheat_tac ctxt) st
  35.187 +    CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st)
  35.188    else error "Cheating requires quick_and_dirty mode!");
  35.189  
  35.190  
  35.191 @@ -195,7 +207,7 @@
  35.192  fun atomize false ctxt =
  35.193        SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
  35.194    | atomize true ctxt =
  35.195 -      EMPTY_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
  35.196 +      CONTEXT_TACTIC o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
  35.197  
  35.198  
  35.199  (* this -- resolve facts directly *)
  35.200 @@ -293,7 +305,7 @@
  35.201  (* intros_tac -- pervasive search spanned by intro rules *)
  35.202  
  35.203  fun gen_intros_tac goals ctxt intros facts =
  35.204 -  goals (insert_tac facts THEN'
  35.205 +  goals (insert_tac ctxt facts THEN'
  35.206        REPEAT_ALL_NEW (resolve_tac ctxt intros))
  35.207      THEN Tactic.distinct_subgoals_tac;
  35.208  
  35.209 @@ -369,7 +381,7 @@
  35.210  val standard_text = Source (Token.make_src ("standard", Position.none) []);
  35.211  val this_text = Basic this;
  35.212  val done_text = Basic (K (SIMPLE_METHOD all_tac));
  35.213 -fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
  35.214 +fun sorry_text int = Basic (fn _ => cheating int);
  35.215  
  35.216  fun finish_text (NONE, immed) = Basic (finish immed)
  35.217    | finish_text (SOME txt, immed) =
  35.218 @@ -455,7 +467,7 @@
  35.219    let
  35.220      val src' = map Token.init_assignable src;
  35.221      val ctxt' = Context_Position.not_really ctxt;
  35.222 -    val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm));
  35.223 +    val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
  35.224    in map Token.closure src' end;
  35.225  
  35.226  val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
  35.227 @@ -473,39 +485,47 @@
  35.228      NONE => false
  35.229    | SOME t => Term.is_dummy_pattern t);
  35.230  
  35.231 -fun STATIC test st =
  35.232 -  if detect_closure_state st then (test (); Seq.single ([], st)) else Seq.empty;
  35.233 +fun STATIC test : context_tactic =
  35.234 +  fn (ctxt, st) =>
  35.235 +    if detect_closure_state st then (test (); Seq.single (Seq.Result (ctxt, st))) else Seq.empty;
  35.236  
  35.237 -fun RUNTIME (tac: cases_tactic) st =
  35.238 -  if detect_closure_state st then Seq.empty else tac st;
  35.239 +fun RUNTIME (tac: context_tactic) (ctxt, st) =
  35.240 +  if detect_closure_state st then Seq.empty else tac (ctxt, st);
  35.241  
  35.242 -fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st)));
  35.243 +fun sleep t = RUNTIME (fn ctxt_st => (OS.Process.sleep t; Seq.single (Seq.Result ctxt_st)));
  35.244  
  35.245  
  35.246  (* evaluate method text *)
  35.247  
  35.248  local
  35.249  
  35.250 -fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) =
  35.251 -  tac st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
  35.252 -
  35.253 -fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) =
  35.254 -  tac st |> Seq.map (pair cases);
  35.255 -
  35.256  val op THEN = Seq.THEN;
  35.257  
  35.258 -val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac);
  35.259 +fun BYPASS_CONTEXT (tac: tactic) =
  35.260 +  fn result =>
  35.261 +    (case result of
  35.262 +      Seq.Error _ => Seq.single result
  35.263 +    | Seq.Result (ctxt, st) => tac st |> CONTEXT ctxt);
  35.264 +
  35.265 +val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac);
  35.266  
  35.267  fun RESTRICT_GOAL i n method =
  35.268 -  BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN
  35.269 +  BYPASS_CONTEXT (PRIMITIVE (Goal.restrict i n)) THEN
  35.270    method THEN
  35.271 -  BYPASS_CASES (PRIMITIVE (Goal.unrestrict i));
  35.272 +  BYPASS_CONTEXT (PRIMITIVE (Goal.unrestrict i));
  35.273  
  35.274  fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method;
  35.275  
  35.276 -fun (method1 THEN_ALL_NEW method2) i (st: cases_state) =
  35.277 -  st |> (method1 i THEN (fn st' =>
  35.278 -    Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st'));
  35.279 +fun (method1 THEN_ALL_NEW method2) i (result : context_state Seq.result) =
  35.280 +  (case result of
  35.281 +    Seq.Error _ => Seq.single result
  35.282 +  | Seq.Result (_, st) =>
  35.283 +      result |> method1 i
  35.284 +      |> Seq.maps (fn result' =>
  35.285 +          (case result' of
  35.286 +            Seq.Error _ => Seq.single result'
  35.287 +          | Seq.Result (_, st') =>
  35.288 +              result' |> Seq.INTERVAL method2 i (i + Thm.nprems_of st' - Thm.nprems_of st))))
  35.289  
  35.290  fun COMBINATOR1 comb [meth] = comb meth
  35.291    | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
  35.292 @@ -514,7 +534,7 @@
  35.293    | combinator Then_All_New =
  35.294        (fn [] => Seq.single
  35.295          | methods =>
  35.296 -            preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)
  35.297 +            preparation THEN (foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1))
  35.298    | combinator Orelse = Seq.FIRST
  35.299    | combinator Try = COMBINATOR1 Seq.TRY
  35.300    | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
  35.301 @@ -525,15 +545,16 @@
  35.302  
  35.303  fun evaluate text ctxt =
  35.304    let
  35.305 -    fun eval (Basic meth) = APPEND_CASES o meth ctxt
  35.306 -      | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
  35.307 +    fun eval0 m facts = Seq.single #> Seq.maps_results (m facts);
  35.308 +    fun eval (Basic m) = eval0 (m ctxt)
  35.309 +      | eval (Source src) = eval0 (method_cmd ctxt src ctxt)
  35.310        | eval (Combinator (_, c, txts)) =
  35.311            let
  35.312              val comb = combinator c;
  35.313              val meths = map eval txts;
  35.314            in fn facts => comb (map (fn meth => meth facts) meths) end;
  35.315      val meth = eval text;
  35.316 -  in fn facts => fn st => meth facts ([], st) end;
  35.317 +  in fn facts => fn ctxt_st => meth facts (Seq.Result ctxt_st) end;
  35.318  
  35.319  end;
  35.320  
  35.321 @@ -711,21 +732,19 @@
  35.322    setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
  35.323    setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
  35.324      "succeed after delay (in seconds)" #>
  35.325 -  setup @{binding "-"} (Scan.succeed (K insert_facts))
  35.326 +  setup @{binding "-"} (Scan.succeed (K (SIMPLE_METHOD all_tac)))
  35.327      "insert current facts, nothing else" #>
  35.328 -  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
  35.329 -    METHOD_CASES (fn _ => fn st =>
  35.330 -      let
  35.331 -        val _ =
  35.332 -          (case drop (Thm.nprems_of st) names of
  35.333 -            [] => ()
  35.334 -          | bad =>
  35.335 -              if detect_closure_state st then ()
  35.336 -              else
  35.337 -                (* FIXME Seq.Error *)
  35.338 -                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
  35.339 -                  Position.here (Position.set_range (Token.range_of bad))));
  35.340 -      in goal_cases_tac ctxt (map Token.content_of names) st end)))
  35.341 +  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ =>
  35.342 +    CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
  35.343 +      (case drop (Thm.nprems_of st) names of
  35.344 +        [] => NONE
  35.345 +      | bad =>
  35.346 +          if detect_closure_state st then NONE
  35.347 +          else
  35.348 +            SOME (fn () => ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
  35.349 +              Position.here (Position.set_range (Token.range_of bad)))))
  35.350 +      |> (fn SOME msg => Seq.single (Seq.Error msg)
  35.351 +           | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
  35.352      "bind cases for goals" #>
  35.353    setup @{binding insert} (Attrib.thms >> (K o insert))
  35.354      "insert theorems, ignoring facts" #>
  35.355 @@ -754,7 +773,7 @@
  35.356        "rotate assumptions of goal" #>
  35.357    setup @{binding tactic} (parse_tactic >> (K o METHOD))
  35.358      "ML tactic as proof method" #>
  35.359 -  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => EMPTY_CASES o tac))
  35.360 +  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
  35.361      "ML tactic as raw proof method");
  35.362  
  35.363  
  35.364 @@ -767,7 +786,7 @@
  35.365  structure Basic_Method: BASIC_METHOD = Method;
  35.366  open Basic_Method;
  35.367  
  35.368 -val METHOD_CASES = Method.METHOD_CASES;
  35.369 +val CONTEXT_METHOD = Method.CONTEXT_METHOD;
  35.370  val METHOD = Method.METHOD;
  35.371  val SIMPLE_METHOD = Method.SIMPLE_METHOD;
  35.372  val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
    36.1 --- a/src/Pure/Isar/obtain.ML	Sat Dec 12 15:37:42 2015 +0100
    36.2 +++ b/src/Pure/Isar/obtain.ML	Sun Dec 13 21:56:15 2015 +0100
    36.3 @@ -266,7 +266,7 @@
    36.4      val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
    36.5      val st = Goal.init (Thm.cterm_of ctxt thesis);
    36.6      val rule =
    36.7 -      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
    36.8 +      (case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of
    36.9          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
   36.10        | SOME th =>
   36.11            check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
   36.12 @@ -413,9 +413,8 @@
   36.13        (SOME before_qed) after_qed
   36.14        [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
   36.15      |> snd
   36.16 -    |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
   36.17 -        Goal.init (Thm.cterm_of ctxt thesis)))
   36.18 -    |> Seq.hd
   36.19 +    |> Proof.refine_singleton
   36.20 +        (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
   36.21    end;
   36.22  
   36.23  in
    37.1 --- a/src/Pure/Isar/proof.ML	Sat Dec 12 15:37:42 2015 +0100
    37.2 +++ b/src/Pure/Isar/proof.ML	Sun Dec 13 21:56:15 2015 +0100
    37.3 @@ -35,8 +35,9 @@
    37.4    val has_bottom_goal: state -> bool
    37.5    val using_facts: thm list -> state -> state
    37.6    val pretty_state: state -> Pretty.T list
    37.7 -  val refine: Method.text -> state -> state Seq.seq
    37.8 -  val refine_end: Method.text -> state -> state Seq.seq
    37.9 +  val refine: Method.text -> state -> state Seq.result Seq.seq
   37.10 +  val refine_end: Method.text -> state -> state Seq.result Seq.seq
   37.11 +  val refine_singleton: Method.text -> state -> state
   37.12    val refine_insert: thm list -> state -> state
   37.13    val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
   37.14    val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   37.15 @@ -90,14 +91,11 @@
   37.16    val end_block: state -> state
   37.17    val begin_notepad: context -> state
   37.18    val end_notepad: state -> context
   37.19 -  val proof: Method.text option -> state -> state Seq.seq
   37.20 -  val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
   37.21 +  val proof: Method.text_range option -> state -> state Seq.result Seq.seq
   37.22    val defer: int -> state -> state
   37.23    val prefer: int -> state -> state
   37.24 -  val apply: Method.text -> state -> state Seq.seq
   37.25 -  val apply_end: Method.text -> state -> state Seq.seq
   37.26 -  val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
   37.27 -  val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
   37.28 +  val apply: Method.text_range -> state -> state Seq.result Seq.seq
   37.29 +  val apply_end: Method.text_range -> state -> state Seq.result Seq.seq
   37.30    val local_qed: Method.text_range option * bool -> state -> state
   37.31    val theorem: Method.text option -> (thm list list -> context -> context) ->
   37.32      (term * term list) list list -> context -> state
   37.33 @@ -424,14 +422,13 @@
   37.34  
   37.35  fun apply_method text ctxt state =
   37.36    find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
   37.37 -    Method.evaluate text ctxt using goal
   37.38 -    |> Seq.map (fn (meth_cases, goal') =>
   37.39 +    Method.evaluate text ctxt using (goal_ctxt, goal)
   37.40 +    |> Seq.map_result (fn (goal_ctxt', goal') =>
   37.41        let
   37.42 -        val goal_ctxt' = goal_ctxt
   37.43 -          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal')
   37.44 -          |> Proof_Context.update_cases meth_cases;
   37.45 +        val goal_ctxt'' = goal_ctxt'
   37.46 +          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
   37.47          val state' = state
   37.48 -          |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed));
   37.49 +          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
   37.50        in state' end));
   37.51  
   37.52  in
   37.53 @@ -439,11 +436,13 @@
   37.54  fun refine text state = apply_method text (context_of state) state;
   37.55  fun refine_end text state = apply_method text (#1 (find_goal state)) state;
   37.56  
   37.57 -fun refine_insert ths =
   37.58 -  Seq.hd o refine (Method.Basic (K (Method.insert ths)));
   37.59 +fun refine_singleton text = refine text #> Seq.the_result "";
   37.60  
   37.61 -fun refine_primitive r =  (* FIXME Seq.Error!? *)
   37.62 -  Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
   37.63 +fun refine_insert ths =
   37.64 +  refine_singleton (Method.Basic (K (Method.insert ths)));
   37.65 +
   37.66 +fun refine_primitive r =
   37.67 +  refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
   37.68  
   37.69  end;
   37.70  
   37.71 @@ -924,17 +923,15 @@
   37.72  (* sub-proofs *)
   37.73  
   37.74  fun proof opt_text =
   37.75 -  assert_backward
   37.76 -  #> refine (the_default Method.standard_text opt_text)
   37.77 -  #> Seq.map
   37.78 -    (using_facts []
   37.79 -      #> enter_forward
   37.80 -      #> open_block
   37.81 -      #> reset_goal);
   37.82 -
   37.83 -fun proof_results arg =
   37.84 -  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
   37.85 -    method_error "initial" (Method.position arg));
   37.86 +  Seq.APPEND
   37.87 +    (assert_backward
   37.88 +      #> refine (the_default Method.standard_text (Method.text opt_text))
   37.89 +      #> Seq.map_result
   37.90 +        (using_facts []
   37.91 +          #> enter_forward
   37.92 +          #> open_block
   37.93 +          #> reset_goal),
   37.94 +     method_error "initial" (Method.position opt_text));
   37.95  
   37.96  fun end_proof bot (prev_pos, (opt_text, immed)) =
   37.97    let
   37.98 @@ -951,8 +948,8 @@
   37.99        |> assert_current_goal true
  37.100        |> using_facts []
  37.101        |> `before_qed |-> (refine o the_default Method.succeed_text)
  37.102 -      |> Seq.maps (refine finish_text)
  37.103 -      |> Seq.make_results, method_error "terminal" terminal_pos)
  37.104 +      |> Seq.maps_results (refine finish_text),
  37.105 +      method_error "terminal" terminal_pos)
  37.106      #> Seq.maps_results (Seq.single o finished_goal finished_pos)
  37.107    end;
  37.108  
  37.109 @@ -966,21 +963,18 @@
  37.110  
  37.111  fun defer i =
  37.112    assert_no_chain #>
  37.113 -  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
  37.114 +  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i)));
  37.115  
  37.116  fun prefer i =
  37.117    assert_no_chain #>
  37.118 -  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
  37.119 -
  37.120 -fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
  37.121 -
  37.122 -fun apply_end text = assert_forward #> refine_end text;
  37.123 +  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i)));
  37.124  
  37.125 -fun apply_results (text, (pos, _)) =
  37.126 -  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
  37.127 +fun apply (text, (pos, _)) =
  37.128 +  Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []),
  37.129 +    method_error "" pos);
  37.130  
  37.131 -fun apply_end_results (text, (pos, _)) =
  37.132 -  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
  37.133 +fun apply_end (text, (pos, _)) =
  37.134 +  Seq.APPEND (assert_forward #> refine_end text, method_error "" pos);
  37.135  
  37.136  
  37.137  
  37.138 @@ -1002,10 +996,9 @@
  37.139    in map (Logic.mk_term o Var) vars end;
  37.140  
  37.141  fun refine_terms n =
  37.142 -  refine (Method.Basic (fn ctxt => EMPTY_CASES o
  37.143 +  refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
  37.144      K (HEADGOAL (PRECISE_CONJUNCTS n
  37.145 -      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
  37.146 -  #> Seq.hd;
  37.147 +      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
  37.148  
  37.149  in
  37.150  
  37.151 @@ -1042,7 +1035,7 @@
  37.152      |> chaining ? (`the_facts #-> using_facts)
  37.153      |> reset_facts
  37.154      |> not (null vars) ? refine_terms (length goal_propss)
  37.155 -    |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
  37.156 +    |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
  37.157    end;
  37.158  
  37.159  fun generic_qed state =
  37.160 @@ -1151,7 +1144,7 @@
  37.161  local
  37.162  
  37.163  fun terminal_proof qeds initial terminal =
  37.164 -  proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
  37.165 +  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
  37.166    #> Seq.the_result "";
  37.167  
  37.168  in
    38.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Dec 12 15:37:42 2015 +0100
    38.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Dec 13 21:56:15 2015 +0100
    38.3 @@ -429,7 +429,7 @@
    38.4      val assms =
    38.5        Proof_Context.get_fact ctxt (Facts.named "local.assms")
    38.6          handle ERROR _ => [];
    38.7 -    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
    38.8 +    val add_prems = Seq.hd o TRY (Method.insert_tac ctxt assms 1);
    38.9      val opt_goal' = Option.map add_prems opt_goal;
   38.10    in
   38.11      filter ctxt (all_facts_of ctxt)
    39.1 --- a/src/Pure/Tools/rule_insts.ML	Sat Dec 12 15:37:42 2015 +0100
    39.2 +++ b/src/Pure/Tools/rule_insts.ML	Sun Dec 13 21:56:15 2015 +0100
    39.3 @@ -306,10 +306,10 @@
    39.4    Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) --
    39.5    Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
    39.6      if null insts andalso null fixes
    39.7 -    then quant (Method.insert_tac facts THEN' tac ctxt thms)
    39.8 +    then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms)
    39.9      else
   39.10        (case thms of
   39.11 -        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts fixes thm)
   39.12 +        [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)
   39.13        | _ => error "Cannot have instantiations with multiple rules")));
   39.14  
   39.15  
    40.1 --- a/src/Pure/simplifier.ML	Sat Dec 12 15:37:42 2015 +0100
    40.2 +++ b/src/Pure/simplifier.ML	Sun Dec 13 21:56:15 2015 +0100
    40.3 @@ -370,12 +370,12 @@
    40.4  fun method_setup more_mods =
    40.5    Method.setup @{binding simp}
    40.6      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
    40.7 -      HEADGOAL (Method.insert_tac facts THEN'
    40.8 +      HEADGOAL (Method.insert_tac ctxt facts THEN'
    40.9          (CHANGED_PROP oo tac) ctxt)))
   40.10      "simplification" #>
   40.11    Method.setup @{binding simp_all}
   40.12      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   40.13 -      ALLGOALS (Method.insert_tac facts) THEN
   40.14 +      ALLGOALS (Method.insert_tac ctxt facts) THEN
   40.15          (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
   40.16      "simplification (all goals)";
   40.17  
    41.1 --- a/src/Pure/tactical.ML	Sat Dec 12 15:37:42 2015 +0100
    41.2 +++ b/src/Pure/tactical.ML	Sun Dec 13 21:56:15 2015 +0100
    41.3 @@ -47,7 +47,7 @@
    41.4    val ALLGOALS: (int -> tactic) -> tactic
    41.5    val SOMEGOAL: (int -> tactic) -> tactic
    41.6    val FIRSTGOAL: (int -> tactic) -> tactic
    41.7 -  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    41.8 +  val HEADGOAL: (int -> tactic) -> tactic
    41.9    val REPEAT_SOME: (int -> tactic) -> tactic
   41.10    val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   41.11    val REPEAT_FIRST: (int -> tactic) -> tactic
   41.12 @@ -358,7 +358,7 @@
   41.13    following usual convention for subgoal-based tactics.*)
   41.14  fun (tac1 THEN_ALL_NEW tac2) i st =
   41.15    st |> (tac1 i THEN (fn st' =>
   41.16 -    Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
   41.17 +    st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));
   41.18  
   41.19  (*Repeatedly dig into any emerging subgoals.*)
   41.20  fun REPEAT_ALL_NEW tac =
    42.1 --- a/src/Tools/induct.ML	Sat Dec 12 15:37:42 2015 +0100
    42.2 +++ b/src/Tools/induct.ML	Sun Dec 13 21:56:15 2015 +0100
    42.3 @@ -71,23 +71,21 @@
    42.4    val rotate_tac: int -> int -> int -> tactic
    42.5    val internalize: Proof.context -> int -> thm -> thm
    42.6    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    42.7 -  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    42.8 -    thm list -> int -> cases_tactic
    42.9 +  val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic
   42.10    val get_inductT: Proof.context -> term option list list -> thm list list
   42.11    val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
   42.12 -    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   42.13 +    bool -> (binding option * (term * bool)) option list list ->
   42.14      (string * typ) list list -> term option list -> thm list option ->
   42.15 -    thm list -> int -> cases_tactic
   42.16 -  val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   42.17 +    thm list -> int -> context_tactic
   42.18 +  val induct_tac: bool -> (binding option * (term * bool)) option list list ->
   42.19      (string * typ) list list -> term option list -> thm list option ->
   42.20 -    thm list -> int -> cases_tactic
   42.21 -  val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
   42.22 -    thm list -> int -> cases_tactic
   42.23 +    thm list -> int -> context_tactic
   42.24 +  val coinduct_tac: term option list -> term option list -> thm option ->
   42.25 +    thm list -> int -> context_tactic
   42.26    val gen_induct_setup: binding ->
   42.27 -   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   42.28 +   (bool -> (binding option * (term * bool)) option list list ->
   42.29      (string * typ) list list -> term option list -> thm list option ->
   42.30 -    thm list -> int -> cases_tactic) ->
   42.31 -   local_theory -> local_theory
   42.32 +    thm list -> int -> context_tactic) -> local_theory -> local_theory
   42.33  end;
   42.34  
   42.35  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
   42.36 @@ -479,33 +477,33 @@
   42.37  
   42.38  in
   42.39  
   42.40 -fun cases_tac ctxt simp insts opt_rule facts =
   42.41 -  let
   42.42 -    fun inst_rule r =
   42.43 -      (if null insts then r
   42.44 -       else
   42.45 -         (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   42.46 -           |> maps (prep_inst ctxt align_left I)
   42.47 -           |> infer_instantiate ctxt) r)
   42.48 -      |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
   42.49 -      |> pair (Rule_Cases.get r);
   42.50 -
   42.51 -    val (opt_rule', facts') =
   42.52 -      (case (opt_rule, facts) of
   42.53 -        (NONE, th :: ths) =>
   42.54 -          if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
   42.55 -          else (opt_rule, facts)
   42.56 -      | _ => (opt_rule, facts));
   42.57 -
   42.58 -    val ruleq =
   42.59 -      (case opt_rule' of
   42.60 -        SOME r => Seq.single (inst_rule r)
   42.61 -      | NONE =>
   42.62 -          (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   42.63 -          |> tap (trace_rules ctxt casesN)
   42.64 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   42.65 -  in
   42.66 -    fn i => fn st =>
   42.67 +fun cases_tac simp insts opt_rule facts i : context_tactic =
   42.68 +  fn (ctxt, st) =>
   42.69 +    let
   42.70 +      fun inst_rule r =
   42.71 +        (if null insts then r
   42.72 +         else
   42.73 +           (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   42.74 +             |> maps (prep_inst ctxt align_left I)
   42.75 +             |> infer_instantiate ctxt) r)
   42.76 +        |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
   42.77 +        |> pair (Rule_Cases.get r);
   42.78 +  
   42.79 +      val (opt_rule', facts') =
   42.80 +        (case (opt_rule, facts) of
   42.81 +          (NONE, th :: ths) =>
   42.82 +            if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
   42.83 +            else (opt_rule, facts)
   42.84 +        | _ => (opt_rule, facts));
   42.85 +  
   42.86 +      val ruleq =
   42.87 +        (case opt_rule' of
   42.88 +          SOME r => Seq.single (inst_rule r)
   42.89 +        | NONE =>
   42.90 +            (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   42.91 +            |> tap (trace_rules ctxt casesN)
   42.92 +            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   42.93 +    in
   42.94        ruleq
   42.95        |> Seq.maps (Rule_Cases.consume ctxt [] facts')
   42.96        |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
   42.97 @@ -513,12 +511,12 @@
   42.98            val rule' = rule
   42.99              |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
  42.100          in
  42.101 -          CASES (Rule_Cases.make_common ctxt
  42.102 +          CONTEXT_CASES (Rule_Cases.make_common ctxt
  42.103                (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  42.104 -            ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
  42.105 -                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
  42.106 +            ((Method.insert_tac ctxt facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
  42.107 +                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) (ctxt, st)
  42.108          end)
  42.109 -  end;
  42.110 +    end;
  42.111  
  42.112  end;
  42.113  
  42.114 @@ -741,8 +739,8 @@
  42.115  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
  42.116    | get_inductP _ _ = [];
  42.117  
  42.118 -fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
  42.119 -  SUBGOAL_CASES (fn (_, i) =>
  42.120 +fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts =
  42.121 +  CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
  42.122      let
  42.123        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  42.124        val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
  42.125 @@ -773,8 +771,8 @@
  42.126            val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
  42.127            val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
  42.128          in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
  42.129 -    in
  42.130 -      fn st =>
  42.131 +
  42.132 +      fun context_tac _ _ =
  42.133          ruleq
  42.134          |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
  42.135          |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
  42.136 @@ -786,7 +784,7 @@
  42.137                  val xs = nth_list arbitrary (j - 1);
  42.138                  val k = nth concls (j - 1) + more_consumes;
  42.139                in
  42.140 -                Method.insert_tac (more_facts @ adefs) THEN'
  42.141 +                Method.insert_tac defs_ctxt (more_facts @ adefs) THEN'
  42.142                    (if simp then
  42.143                       rotate_tac k (length adefs) THEN'
  42.144                       arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
  42.145 @@ -794,17 +792,19 @@
  42.146                       arbitrary_tac defs_ctxt k xs)
  42.147                 end)
  42.148              THEN' inner_atomize_tac defs_ctxt) j))
  42.149 -          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
  42.150 +          THEN' atomize_tac defs_ctxt) i st
  42.151 +        |> Seq.maps (fn st' =>
  42.152                guess_instance ctxt (internalize ctxt more_consumes rule) i st'
  42.153                |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  42.154                |> Seq.maps (fn rule' =>
  42.155 -                CASES (rule_cases ctxt rule' cases)
  42.156 +                CONTEXT_CASES (rule_cases ctxt rule' cases)
  42.157                    (resolve_tac ctxt [rule'] i THEN
  42.158 -                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
  42.159 -      end)
  42.160 -      THEN_ALL_NEW_CASES
  42.161 +                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
  42.162 +    in
  42.163 +      (context_tac CONTEXT_THEN_ALL_NEW
  42.164          ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
  42.165 -         THEN_ALL_NEW rulify_tac ctxt);
  42.166 +         THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
  42.167 +    end)
  42.168  
  42.169  val induct_tac = gen_induct_tac I;
  42.170  
  42.171 @@ -831,15 +831,15 @@
  42.172  
  42.173  in
  42.174  
  42.175 -fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
  42.176 -  let
  42.177 -    fun inst_rule r =
  42.178 -      if null inst then `Rule_Cases.get r
  42.179 -      else
  42.180 -        infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
  42.181 -        |> pair (Rule_Cases.get r);
  42.182 -  in
  42.183 -    fn st =>
  42.184 +fun coinduct_tac inst taking opt_rule facts =
  42.185 +  CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
  42.186 +    let
  42.187 +      fun inst_rule r =
  42.188 +        if null inst then `Rule_Cases.get r
  42.189 +        else
  42.190 +          infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
  42.191 +          |> pair (Rule_Cases.get r);
  42.192 +    in
  42.193        (case opt_rule of
  42.194          SOME r => Seq.single (inst_rule r)
  42.195        | NONE =>
  42.196 @@ -851,10 +851,10 @@
  42.197          guess_instance ctxt rule i st
  42.198          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  42.199          |> Seq.maps (fn rule' =>
  42.200 -          CASES (Rule_Cases.make_common ctxt
  42.201 +          CONTEXT_CASES (Rule_Cases.make_common ctxt
  42.202                (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  42.203 -            (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
  42.204 -  end);
  42.205 +            (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
  42.206 +    end);
  42.207  
  42.208  end;
  42.209  
  42.210 @@ -919,8 +919,8 @@
  42.211      (Scan.lift (Args.mode no_simpN) --
  42.212        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
  42.213          (arbitrary -- taking -- Scan.option induct_rule)) >>
  42.214 -      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
  42.215 -        Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
  42.216 +      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn _ => fn facts =>
  42.217 +        Seq.DETERM (tac (not no_simp) insts arbitrary taking opt_rule facts 1)))
  42.218      "induction on types or predicates/sets";
  42.219  
  42.220  val _ =
  42.221 @@ -928,15 +928,15 @@
  42.222      (Method.local_setup @{binding cases}
  42.223        (Scan.lift (Args.mode no_simpN) --
  42.224          (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
  42.225 -        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
  42.226 -          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
  42.227 -            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
  42.228 +        (fn (no_simp, (insts, opt_rule)) => fn _ =>
  42.229 +          CONTEXT_METHOD (fn facts =>
  42.230 +            Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1))))
  42.231        "case analysis on types or predicates/sets" #>
  42.232      gen_induct_setup @{binding induct} induct_tac #>
  42.233       Method.local_setup @{binding coinduct}
  42.234        (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
  42.235 -        (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
  42.236 -          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
  42.237 +        (fn ((insts, taking), opt_rule) => fn _ => fn facts =>
  42.238 +          Seq.DETERM (coinduct_tac insts taking opt_rule facts 1)))
  42.239        "coinduction on types or predicates/sets");
  42.240  
  42.241  end;
    43.1 --- a/src/Tools/induction.ML	Sat Dec 12 15:37:42 2015 +0100
    43.2 +++ b/src/Tools/induction.ML	Sun Dec 13 21:56:15 2015 +0100
    43.3 @@ -7,10 +7,9 @@
    43.4  
    43.5  signature INDUCTION =
    43.6  sig
    43.7 -  val induction_tac: Proof.context -> bool ->
    43.8 -    (binding option * (term * bool)) option list list ->
    43.9 +  val induction_tac: bool -> (binding option * (term * bool)) option list list ->
   43.10      (string * typ) list list -> term option list -> thm list option ->
   43.11 -    thm list -> int -> cases_tactic
   43.12 +    thm list -> int -> context_tactic
   43.13  end
   43.14  
   43.15  structure Induction: INDUCTION =