prefer tactics with explicit context;
authorwenzelm
Sat Jul 18 21:44:18 2015 +0200 (2015-07-18)
changeset 60757c09598a97436
parent 60756 f122140b7195
child 60758 d8d85a8172b5
prefer tactics with explicit context;
src/HOL/Library/bnf_lfp_countable.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
src/Provers/classical.ML
     1.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 21:25:55 2015 +0200
     1.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 21:44:18 2015 +0200
     1.3 @@ -24,8 +24,8 @@
     1.4  val countableS = @{sort countable};
     1.5  
     1.6  fun nchotomy_tac ctxt nchotomy =
     1.7 -  HEADGOAL (rtac ctxt (nchotomy RS @{thm all_reg[rotated]}) THEN'
     1.8 -    REPEAT_ALL_NEW (resolve0_tac [allI, impI] ORELSE' eresolve0_tac [exE, disjE]));
     1.9 +  HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
    1.10 +    REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
    1.11  
    1.12  fun meta_spec_mp_tac ctxt 0 = K all_tac
    1.13    | meta_spec_mp_tac ctxt depth =
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:25:55 2015 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:44:18 2015 +0200
     2.3 @@ -247,7 +247,7 @@
     2.4            val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
     2.5            val goal = mk_Trueprop_mem (bd_bd', ordIso);
     2.6          in
     2.7 -          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
     2.8 +          (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
     2.9              |> Thm.close_derivation))
    2.10          end
    2.11        else
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4    val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
     3.5    val mk_simple_wit_tac: Proof.context -> thm list -> tactic
     3.6    val mk_simplified_set_tac: Proof.context -> thm -> tactic
     3.7 -  val bd_ordIso_natLeq_tac: tactic
     3.8 +  val bd_ordIso_natLeq_tac: Proof.context -> tactic
     3.9  end;
    3.10  
    3.11  structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
    3.12 @@ -233,7 +233,7 @@
    3.13    rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
    3.14  
    3.15  fun mk_simple_wit_tac ctxt wit_thms =
    3.16 -  ALLGOALS (assume_tac ctxt ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
    3.17 +  ALLGOALS (assume_tac ctxt ORELSE' eresolve_tac ctxt (@{thm emptyE} :: wit_thms));
    3.18  
    3.19  val csum_thms =
    3.20    @{thms csum_cong1 csum_cong2 csum_cong  csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
    3.21 @@ -248,8 +248,8 @@
    3.22    unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
    3.23    unfold_thms_tac ctxt simplified_set_simps THEN rtac ctxt refl 1;
    3.24  
    3.25 -val bd_ordIso_natLeq_tac =
    3.26 -  HEADGOAL (REPEAT_DETERM o resolve0_tac
    3.27 +fun bd_ordIso_natLeq_tac ctxt =
    3.28 +  HEADGOAL (REPEAT_DETERM o resolve_tac ctxt
    3.29      (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
    3.30  
    3.31  end;
     4.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     4.3 @@ -55,13 +55,15 @@
     4.4    (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
     4.5     REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
     4.6  fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
     4.7 -fun mk_in_mono_tac ctxt n = if n = 0 then rtac ctxt subset_UNIV 1
     4.8 -  else (rtac ctxt subsetI THEN'
     4.9 -  rtac ctxt CollectI) 1 THEN
    4.10 -  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN
    4.11 -  REPEAT_DETERM_N (n - 1)
    4.12 -    ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
    4.13 -  (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
    4.14 +
    4.15 +fun mk_in_mono_tac ctxt n =
    4.16 +  if n = 0 then rtac ctxt subset_UNIV 1
    4.17 +  else
    4.18 +   (rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN
    4.19 +   REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN
    4.20 +   REPEAT_DETERM_N (n - 1)
    4.21 +     ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
    4.22 +   (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
    4.23  
    4.24  fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
    4.25    let
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     5.3 @@ -128,7 +128,7 @@
     5.4        HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' assume_tac ctxt THEN'
     5.5        REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN'
     5.6          assume_tac ctxt THEN' rotate_tac ~1 THEN'
     5.7 -        etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
     5.8 +        etac ctxt (rotate_prems 1 notE) THEN' eresolve_tac ctxt distinct_disc));
     5.9    in
    5.10      HEADGOAL Goal.conjunction_tac THEN
    5.11      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI THEN' dtac ctxt (rel_sel RS iffD1) THEN'
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     6.3 @@ -117,7 +117,7 @@
     6.4    dtac ctxt (coalg_def RS iffD1) 1 THEN
     6.5    REPEAT_DETERM (etac ctxt conjE 1) THEN
     6.6    EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
     6.7 -  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN assume_tac ctxt 1;
     6.8 +  REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1;
     6.9  
    6.10  fun mk_mor_elim_tac ctxt mor_def =
    6.11    (dtac ctxt (mor_def RS iffD1) THEN'
    6.12 @@ -226,7 +226,7 @@
    6.13      fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
    6.14        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
    6.15          etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
    6.16 -        REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
    6.17 +        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
    6.18          rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
    6.19          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
    6.20            REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
    6.21 @@ -246,7 +246,7 @@
    6.22        EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
    6.23          etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
    6.24          dtac ctxt (in_rel RS @{thm iffD1}),
    6.25 -        REPEAT_DETERM o eresolve0_tac ([CollectE, conjE, exE] @
    6.26 +        REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
    6.27            @{thms CollectE Collect_split_in_rel_leE}),
    6.28          rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
    6.29          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
    6.30 @@ -654,7 +654,7 @@
    6.31  
    6.32  fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
    6.33    EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
    6.34 -    REPEAT_DETERM o eresolve0_tac [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
    6.35 +    REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
    6.36      etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
    6.37      rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
    6.38      EVERY' (map (fn equiv_LSBIS =>
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     7.3 @@ -126,7 +126,7 @@
     7.4      fun mor_tac (set_map, map_comp_id) =
     7.5        EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
     7.6          rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
     7.7 -         REPEAT o eresolve0_tac [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
     7.8 +         REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
     7.9        CONJ_WRAP' (fn thm =>
    7.10          FIRST' [rtac ctxt subset_UNIV,
    7.11            (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
    7.12 @@ -172,14 +172,14 @@
    7.13          rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
    7.14      val alg_tac =
    7.15        CONJ_WRAP' (fn (set_maps, alg_set) =>
    7.16 -        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt set_mp,
    7.17 +        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
    7.18            rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
    7.19            rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
    7.20        (set_mapss ~~ alg_sets);
    7.21  
    7.22      val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
    7.23        CONJ_WRAP' (fn (set_maps, alg_set) =>
    7.24 -        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
    7.25 +        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
    7.26            etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
    7.27            EVERY' (map set_tac (drop m set_maps))])
    7.28        (set_mapss ~~ alg_sets);
    7.29 @@ -257,7 +257,7 @@
    7.30        rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite},
    7.31        rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order,
    7.32        rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq},
    7.33 -      resolve0_tac @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
    7.34 +      resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
    7.35        rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite];
    7.36    in
    7.37      (rtac ctxt induct THEN'
    7.38 @@ -276,7 +276,7 @@
    7.39  
    7.40      fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
    7.41        rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
    7.42 -      REPEAT_DETERM o eresolve0_tac [CollectE, conjE], etac ctxt alg_set,
    7.43 +      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
    7.44        REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)];
    7.45    in
    7.46      (rtac ctxt induct THEN'
    7.47 @@ -290,9 +290,9 @@
    7.48      val n = length min_algs;
    7.49      fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
    7.50        [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
    7.51 -       etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve0_tac set_bds];
    7.52 +       etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
    7.53      fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
    7.54 -      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
    7.55 +      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
    7.56          EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
    7.57          rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
    7.58          rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
    7.59 @@ -339,9 +339,9 @@
    7.60      val mor_tac =
    7.61        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
    7.62      fun alg_epi_tac ((alg_set, str_init_def), set_map) =
    7.63 -      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt CollectI,
    7.64 +      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
    7.65          rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
    7.66 -        etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve0_tac set_map,
    7.67 +        etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
    7.68            rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
    7.69            assume_tac ctxt]];
    7.70    in
    7.71 @@ -358,7 +358,7 @@
    7.72      EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
    7.73        REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
    7.74        REPEAT_DETERM_N n o assume_tac ctxt,
    7.75 -      rtac ctxt impI, REPEAT_DETERM o eresolve0_tac [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
    7.76 +      rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
    7.77        rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
    7.78        rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
    7.79        SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
    7.80 @@ -381,7 +381,7 @@
    7.81  
    7.82      fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
    7.83        EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
    7.84 -        REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
    7.85 +        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
    7.86          REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
    7.87          rtac ctxt trans, mor_tac morE in_mono,
    7.88          rtac ctxt trans, cong_tac ct map_cong0,
    7.89 @@ -400,7 +400,7 @@
    7.90      val n = length least_min_algs;
    7.91  
    7.92      fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
    7.93 -      REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
    7.94 +      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
    7.95        REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
    7.96        rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
    7.97        REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
    7.98 @@ -449,7 +449,7 @@
    7.99    let
   7.100      fun mk_unique type_def =
   7.101        EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
   7.102 -        rtac ctxt ballI, resolve0_tac init_unique_mors,
   7.103 +        rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
   7.104          EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
   7.105          rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
   7.106          rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
     8.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
     8.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
     8.3 @@ -87,7 +87,7 @@
     8.4  
     8.5  fun mk_exhaust_sel_tac ctxt n exhaust_disc collapses =
     8.6    mk_exhaust_disc_or_sel_tac ctxt n exhaust_disc collapses ORELSE
     8.7 -  HEADGOAL (etac ctxt meta_mp THEN' resolve0_tac collapses);
     8.8 +  HEADGOAL (etac ctxt meta_mp THEN' resolve_tac ctxt collapses);
     8.9  
    8.10  fun mk_collapse_tac ctxt m discD sels =
    8.11    HEADGOAL (dtac ctxt discD THEN'
     9.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:25:55 2015 +0200
     9.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:44:18 2015 +0200
     9.3 @@ -149,7 +149,7 @@
     9.4            NONE => NONE
     9.5          | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
     9.6      val indrule' = cterm_instantiate insts indrule;
     9.7 -  in resolve0_tac [indrule'] i end);
     9.8 +  in resolve_tac ctxt [indrule'] i end);
     9.9  
    9.10  
    9.11  (* perform exhaustive case analysis on last parameter of subgoal i *)
    10.1 --- a/src/Provers/classical.ML	Sat Jul 18 21:25:55 2015 +0200
    10.2 +++ b/src/Provers/classical.ML	Sat Jul 18 21:44:18 2015 +0200
    10.3 @@ -157,7 +157,7 @@
    10.4        val rule'' =
    10.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
    10.6            if i = 1 orelse redundant_hyp goal
    10.7 -          then eresolve0_tac [thin_rl] i
    10.8 +          then eresolve_tac ctxt [thin_rl] i
    10.9            else all_tac))
   10.10          |> Seq.hd
   10.11          |> Drule.zero_var_indexes;