less hermetic tactics
authortraytel
Fri Jan 31 10:02:36 2014 +0100 (2014-01-31)
changeset 551975a54ed681ba2
parent 55196 a823137bcd87
child 55198 7a538e58b64e
less hermetic tactics
src/HOL/Library/bnf_decl.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_tactics.ML
     1.1 --- a/src/HOL/Library/bnf_decl.ML	Thu Jan 30 22:55:52 2014 +0100
     1.2 +++ b/src/HOL/Library/bnf_decl.ML	Fri Jan 31 10:02:36 2014 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4        user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
     1.5        lthy;
     1.6  
     1.7 -    fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
     1.8 +    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
     1.9      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    1.10      val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    1.11  
    1.12 @@ -81,7 +81,8 @@
    1.13        ||> `Local_Theory.restore;
    1.14  
    1.15      fun mk_wit_thms set_maps =
    1.16 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
    1.17 +      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    1.18 +        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
    1.19        |> Conjunction.elim_balanced (length wit_goals)
    1.20        |> map2 (Conjunction.elim_balanced o length) wit_goalss
    1.21        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jan 30 22:55:52 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Fri Jan 31 10:02:36 2014 +0100
     2.3 @@ -198,7 +198,7 @@
     2.4            val single_set_bd_thmss =
     2.5              map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
     2.6          in
     2.7 -          map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
     2.8 +          map2 (fn set_alt => fn single_set_bds => fn ctxt =>
     2.9              mk_comp_set_bd_tac ctxt set_alt single_set_bds)
    2.10            set_alt_thms single_set_bd_thmss
    2.11          end;
    2.12 @@ -251,7 +251,7 @@
    2.13        |> minimize_wits
    2.14        |> map (fn (frees, t) => fold absfree frees t);
    2.15  
    2.16 -    fun wit_tac {context = ctxt, prems = _} =
    2.17 +    fun wit_tac ctxt =
    2.18        mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
    2.19          (maps wit_thms_of_bnf inners);
    2.20  
    2.21 @@ -301,10 +301,10 @@
    2.22        (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
    2.23  
    2.24      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
    2.25 -    fun map_comp0_tac {context = ctxt, prems = _} =
    2.26 +    fun map_comp0_tac ctxt =
    2.27        unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
    2.28          @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
    2.29 -    fun map_cong0_tac {context = ctxt, prems = _} =
    2.30 +    fun map_cong0_tac ctxt =
    2.31        mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    2.32      val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
    2.33      fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    2.34 @@ -322,7 +322,7 @@
    2.35          Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
    2.36        end;
    2.37  
    2.38 -    fun le_rel_OO_tac {context = ctxt, prems = _} =
    2.39 +    fun le_rel_OO_tac ctxt =
    2.40        EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
    2.41        unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
    2.42  
    2.43 @@ -393,10 +393,10 @@
    2.44      val bd = mk_bd_of_bnf Ds As bnf;
    2.45  
    2.46      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
    2.47 -    fun map_comp0_tac {context = ctxt, prems = _} =
    2.48 +    fun map_comp0_tac ctxt =
    2.49        unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
    2.50          @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
    2.51 -    fun map_cong0_tac {context = ctxt, prems = _} =
    2.52 +    fun map_cong0_tac ctxt =
    2.53        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    2.54      val set_map0_tacs =
    2.55        if Config.get lthy quick_and_dirty then
    2.56 @@ -478,7 +478,7 @@
    2.57  
    2.58      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
    2.59      fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
    2.60 -    fun map_cong0_tac {context = ctxt, prems = _} =
    2.61 +    fun map_cong0_tac ctxt =
    2.62        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    2.63      val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf));
    2.64      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    2.65 @@ -628,7 +628,7 @@
    2.66      val set_bds =
    2.67        map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
    2.68  
    2.69 -    fun mk_tac thm {context = ctxt, prems = _} =
    2.70 +    fun mk_tac thm ctxt =
    2.71        (rtac (unfold_all ctxt thm) THEN'
    2.72        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
    2.73  
    2.74 @@ -640,7 +640,7 @@
    2.75  
    2.76      val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    2.77  
    2.78 -    fun wit_tac {context = ctxt, prems = _} =
    2.79 +    fun wit_tac ctxt =
    2.80        mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
    2.81  
    2.82      val (bnf', lthy') =
     3.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jan 30 22:55:52 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 31 10:02:36 2014 +0100
     3.3 @@ -106,7 +106,7 @@
     3.4      binding -> binding -> binding list ->
     3.5      (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
     3.6      string * term list *
     3.7 -    ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
     3.8 +    ((Proof.context -> thm list -> tactic) option * term list list) *
     3.9      ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
    3.10      local_theory * thm list
    3.11  
    3.12 @@ -123,8 +123,8 @@
    3.13          (typ list -> typ list -> typ list -> term))) * local_theory
    3.14  
    3.15    val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    3.16 -    ({prems: thm list, context: Proof.context} -> tactic) list ->
    3.17 -    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
    3.18 +    (Proof.context -> tactic) list ->
    3.19 +    (Proof.context -> tactic) -> typ list option -> binding ->
    3.20      binding -> binding list ->
    3.21      (((((binding * typ) * term) * term list) * term) * term list) * term option ->
    3.22      local_theory -> bnf * local_theory
    3.23 @@ -1021,7 +1021,7 @@
    3.24          map wit_goal (0 upto live - 1)
    3.25        end;
    3.26  
    3.27 -    val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
    3.28 +    fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
    3.29  
    3.30      val wit_goalss =
    3.31        (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
    3.32 @@ -1132,7 +1132,7 @@
    3.33                  (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
    3.34            in
    3.35              Goal.prove_sorry lthy [] [] in_bd_goal
    3.36 -              (mk_in_bd_tac live surj_imp_ordLeq_inst
    3.37 +              (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst
    3.38                  (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
    3.39                  (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
    3.40                  bd_Card_order bd_Cinfinite bd_Cnotzero)
    3.41 @@ -1151,8 +1151,9 @@
    3.42              val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
    3.43            in
    3.44              Goal.prove_sorry lthy [] [] goal
    3.45 -              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
    3.46 -                (Lazy.force map_comp) (map Lazy.force set_map))
    3.47 +              (fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
    3.48 +                (#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
    3.49 +                (map Lazy.force set_map))
    3.50              |> Thm.close_derivation
    3.51            end;
    3.52  
    3.53 @@ -1203,8 +1204,9 @@
    3.54              val rhs = mk_conversep (Term.list_comb (rel, Rs));
    3.55              val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
    3.56              val le_thm = Goal.prove_sorry lthy [] [] le_goal
    3.57 -              (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
    3.58 -                (Lazy.force map_comp) (map Lazy.force set_map))
    3.59 +              (fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
    3.60 +                (Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
    3.61 +                (map Lazy.force set_map))
    3.62                |> Thm.close_derivation
    3.63              val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
    3.64            in
    3.65 @@ -1218,8 +1220,8 @@
    3.66          fun mk_rel_OO () =
    3.67            Goal.prove_sorry lthy [] []
    3.68              (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
    3.69 -            (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
    3.70 -              (Lazy.force map_comp) (map Lazy.force set_map))
    3.71 +            (fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
    3.72 +              (#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
    3.73            |> Thm.close_derivation
    3.74            |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
    3.75  
    3.76 @@ -1254,7 +1256,8 @@
    3.77            in
    3.78              Goal.prove_sorry lthy [] []
    3.79                (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
    3.80 -              (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map))
    3.81 +              (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
    3.82 +                (map Lazy.force set_map))
    3.83              |> Thm.close_derivation
    3.84            end;
    3.85  
    3.86 @@ -1271,8 +1274,9 @@
    3.87            in
    3.88              Goal.prove_sorry lthy [] []
    3.89                (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
    3.90 -              (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
    3.91 -                (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp))
    3.92 +              (fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
    3.93 +                (Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
    3.94 +                (Lazy.force map_comp))
    3.95              |> Thm.close_derivation
    3.96            end;
    3.97  
    3.98 @@ -1308,22 +1312,22 @@
    3.99  fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
   3.100    (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
   3.101    let
   3.102 -    fun mk_wits_tac set_maps =
   3.103 -      K (TRYALL Goal.conjunction_tac) THEN'
   3.104 +    fun mk_wits_tac ctxt set_maps =
   3.105 +      TRYALL Goal.conjunction_tac THEN
   3.106        (case triv_tac_opt of
   3.107 -        SOME tac => tac set_maps
   3.108 -      | NONE => fn {context = ctxt, prems} =>
   3.109 -          unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems});
   3.110 +        SOME tac => tac ctxt set_maps
   3.111 +      | NONE => unfold_thms_tac ctxt one_step_defs THEN wit_tac ctxt);
   3.112      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
   3.113      fun mk_wit_thms set_maps =
   3.114 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
   3.115 +      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
   3.116 +        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
   3.117          |> Conjunction.elim_balanced (length wit_goals)
   3.118          |> map2 (Conjunction.elim_balanced o length) wit_goalss
   3.119          |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
   3.120    in
   3.121      map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
   3.122 -      goals (map (fn tac => fn {context = ctxt, prems} =>
   3.123 -        unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs)
   3.124 +      goals (map (fn tac => fn {context = ctxt, prems = _} =>
   3.125 +        unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
   3.126      |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
   3.127    end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
   3.128  
   3.129 @@ -1332,7 +1336,7 @@
   3.130      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
   3.131      fun mk_triv_wit_thms tac set_maps =
   3.132        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
   3.133 -        (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps)
   3.134 +        (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
   3.135          |> Conjunction.elim_balanced (length wit_goals)
   3.136          |> map2 (Conjunction.elim_balanced o length) wit_goalss
   3.137          |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
     4.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
     4.3 @@ -15,25 +15,20 @@
     4.4    val mk_in_mono_tac: int -> tactic
     4.5    val mk_set_map: thm -> thm
     4.6  
     4.7 -  val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     4.8 -    {prems: thm list, context: Proof.context} -> tactic
     4.9 +  val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
    4.10    val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
    4.11 -  val mk_rel_OO_le_tac: thm list -> thm -> thm -> thm -> thm list ->
    4.12 -    {prems: thm list, context: Proof.context} -> tactic
    4.13 +  val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
    4.14    val mk_rel_conversep_tac: thm -> thm -> tactic
    4.15 -  val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
    4.16 -    {prems: thm list, context: Proof.context} -> tactic
    4.17 +  val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
    4.18    val mk_rel_mono_tac: thm list -> thm -> tactic
    4.19 -  val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    4.20 +  val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
    4.21  
    4.22 -  val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
    4.23 -    {prems: thm list, context: Proof.context} -> tactic
    4.24 +  val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
    4.25  
    4.26 -  val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm ->
    4.27 -    thm -> {prems: thm list, context: Proof.context} -> tactic
    4.28 +  val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
    4.29 +    thm -> thm -> thm -> thm -> tactic
    4.30  
    4.31 -  val mk_trivial_wit_tac: thm list -> thm list -> {prems: thm list, context: Proof.context} ->
    4.32 -    tactic
    4.33 +  val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
    4.34  end;
    4.35  
    4.36  structure BNF_Def_Tactics : BNF_DEF_TACTICS =
    4.37 @@ -67,8 +62,7 @@
    4.38      rtac set_map0) set_map0s) THEN'
    4.39    rtac @{thm image_empty}) 1;
    4.40  
    4.41 -fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
    4.42 -  {context = ctxt, prems = _} =
    4.43 +fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
    4.44    let
    4.45      val n = length set_maps;
    4.46      val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
    4.47 @@ -120,8 +114,7 @@
    4.48        rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
    4.49    end;
    4.50  
    4.51 -fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
    4.52 -  {context = ctxt, prems = _} =
    4.53 +fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
    4.54    let
    4.55      val n = length set_maps;
    4.56      val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
    4.57 @@ -146,8 +139,7 @@
    4.58      rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
    4.59      REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
    4.60  
    4.61 -fun mk_rel_OO_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
    4.62 -  {context = ctxt, prems = _} =
    4.63 +fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
    4.64    let
    4.65      val n = length set_maps;
    4.66      fun in_tac nthO_in = rtac CollectI THEN'
    4.67 @@ -183,7 +175,7 @@
    4.68          in_tac @{thm sndOp_in}] 1
    4.69    end;
    4.70  
    4.71 -fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
    4.72 +fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
    4.73    if null set_maps then atac 1
    4.74    else
    4.75      unfold_tac ctxt [in_rel] THEN
    4.76 @@ -194,8 +186,7 @@
    4.77          (etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
    4.78        set_maps] 1;
    4.79  
    4.80 -fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
    4.81 -  {context = ctxt, prems = _} =
    4.82 +fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
    4.83    let
    4.84      val n = length set_maps;
    4.85      val in_tac = if n = 0 then rtac UNIV_I else
    4.86 @@ -216,8 +207,8 @@
    4.87          REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
    4.88    end;
    4.89  
    4.90 -fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
    4.91 -  bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
    4.92 +fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
    4.93 +  bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
    4.94    if live = 0 then
    4.95      rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
    4.96        ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
    4.97 @@ -278,7 +269,7 @@
    4.98             map_comp RS sym, map_id])] 1
    4.99    end;
   4.100  
   4.101 -fun mk_trivial_wit_tac wit_defs set_maps {context = ctxt, prems = _} =
   4.102 +fun mk_trivial_wit_tac ctxt wit_defs set_maps =
   4.103    unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
   4.104      dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
   4.105  
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 30 22:55:52 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 31 10:02:36 2014 +0100
     5.3 @@ -696,7 +696,8 @@
     5.4              map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
     5.5                singleton (Proof_Context.export names_lthy lthy)
     5.6                  (Goal.prove_sorry lthy [] [] goal
     5.7 -                  (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
     5.8 +                  (fn {context = ctxt, prems = _} => mk_hset_rec_minimal_tac ctxt m cts hset_rec_0s
     5.9 +                    hset_rec_Sucs))
    5.10                |> Thm.close_derivation)
    5.11              goals ctss hset_rec_0ss' hset_rec_Sucss'
    5.12            end;
    5.13 @@ -711,7 +712,8 @@
    5.14        in
    5.15          map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
    5.16            Goal.prove_sorry lthy [] [] goal
    5.17 -            (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
    5.18 +            (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n hset_defs
    5.19 +              hset_rec_minimal)
    5.20            |> Thm.close_derivation)
    5.21          goals hset_defss' hset_rec_minimal_thms
    5.22        end;
    5.23 @@ -830,7 +832,8 @@
    5.24          Goal.prove_sorry lthy [] []
    5.25            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
    5.26              (Logic.list_implies ([coalg_prem, mor_prem], concl)))
    5.27 -          (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
    5.28 +          (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
    5.29 +            morE_thms coalg_in_thms)
    5.30          |> Thm.close_derivation
    5.31        end;
    5.32  
    5.33 @@ -852,7 +855,7 @@
    5.34          Goal.prove_sorry lthy [] []
    5.35            (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
    5.36              (Logic.mk_implies (prem, concl)))
    5.37 -          (mk_bis_Union_tac bis_def in_mono'_thms)
    5.38 +          (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
    5.39          |> Thm.close_derivation
    5.40        end;
    5.41  
    5.42 @@ -1193,7 +1196,8 @@
    5.43      val coalgT_thm =
    5.44        Goal.prove_sorry lthy [] []
    5.45          (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
    5.46 -        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
    5.47 +        (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
    5.48 +          (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
    5.49        |> Thm.close_derivation;
    5.50  
    5.51      val timer = time (timer "Tree coalgebra");
    5.52 @@ -1557,7 +1561,7 @@
    5.53        Goal.prove_sorry lthy [] []
    5.54          (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
    5.55            HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
    5.56 -        (mk_mor_beh_tac m mor_def mor_cong_thm
    5.57 +        (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
    5.58            beh_defs carT_defs strT_defs isNode_defs
    5.59            to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
    5.60            length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
    5.61 @@ -1709,14 +1713,15 @@
    5.62          val mor_Rep =
    5.63            Goal.prove_sorry lthy [] []
    5.64              (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
    5.65 -            (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
    5.66 -              map_comp_id_thms map_cong0L_thms)
    5.67 +            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
    5.68 +              Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
    5.69            |> Thm.close_derivation;
    5.70  
    5.71          val mor_Abs =
    5.72            Goal.prove_sorry lthy [] []
    5.73              (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
    5.74 -            (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses)
    5.75 +            (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
    5.76 +              Abs_inverses)
    5.77            |> Thm.close_derivation;
    5.78        in
    5.79          (mor_Rep, mor_Abs)
    5.80 @@ -1863,7 +1868,8 @@
    5.81        in
    5.82          map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
    5.83            Goal.prove_sorry lthy [] [] goal
    5.84 -            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
    5.85 +            (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
    5.86 +              map_cong0L unfold_o_dtor_thms)
    5.87            |> Thm.close_derivation)
    5.88            goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
    5.89        end;
    5.90 @@ -1948,7 +1954,8 @@
    5.91        in
    5.92          map3 (fn goal => fn unfold => fn map_cong0 =>
    5.93            Goal.prove_sorry lthy [] [] goal
    5.94 -            (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
    5.95 +            (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
    5.96 +              corec_Inl_sum_thms)
    5.97            |> Thm.close_derivation)
    5.98          goals dtor_unfold_thms map_cong0s
    5.99        end;
   5.100 @@ -1963,7 +1970,8 @@
   5.101        in
   5.102          Goal.prove_sorry lthy [] []
   5.103            (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
   5.104 -          (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm)
   5.105 +          (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
   5.106 +            corec_Inl_sum_thms unfold_unique_mor_thm)
   5.107            |> Thm.close_derivation
   5.108        end;
   5.109  
   5.110 @@ -2278,7 +2286,8 @@
   5.111            in
   5.112              map2 (fn goal => fn induct =>
   5.113                Goal.prove_sorry lthy [] [] goal
   5.114 -                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_mapss) wit_thms)
   5.115 +                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
   5.116 +                  (flat set_mapss) wit_thms)
   5.117                |> Thm.close_derivation)
   5.118              goals dtor_hset_induct_thms
   5.119              |> map split_conj_thm
   5.120 @@ -2362,7 +2371,7 @@
   5.121              Goal.prove_sorry lthy [] []
   5.122                (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
   5.123                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
   5.124 -                  mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt)
   5.125 +                  mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
   5.126                |> Thm.close_derivation
   5.127            end;
   5.128  
   5.129 @@ -2444,7 +2453,8 @@
   5.130                map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
   5.131                  singleton (Proof_Context.export names_lthy lthy)
   5.132                    (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   5.133 -                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss))
   5.134 +                    (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
   5.135 +                      dtor_Jmap_thms set_mapss))
   5.136                  |> Thm.close_derivation)
   5.137                goals ctss hset_rec_0ss' hset_rec_Sucss';
   5.138            in
   5.139 @@ -2586,7 +2596,7 @@
   5.140        val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
   5.141        val zip_setss = mk_Jsetss passiveABs |> transpose;
   5.142  
   5.143 -      val Jrel_coinduct_tac =
   5.144 +      fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
   5.145          let
   5.146            fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
   5.147              let
   5.148 @@ -2611,13 +2621,13 @@
   5.149              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   5.150                (map6 (mk_helper_coind_concl false)
   5.151                activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
   5.152 -          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
   5.153 -            map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms;
   5.154            fun mk_helper_coind_thms vars concl =
   5.155              Goal.prove_sorry lthy [] []
   5.156                (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
   5.157                  (Logic.list_implies (helper_prems, concl)))
   5.158 -              helper_coind_tac
   5.159 +              (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m
   5.160 +                dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss
   5.161 +                dtor_unfold_thms dtor_Jmap_thms)
   5.162              |> Thm.close_derivation
   5.163              |> split_conj_thm;
   5.164            val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
   5.165 @@ -2641,13 +2651,14 @@
   5.166                Goal.prove_sorry lthy [] []
   5.167                  (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
   5.168                    (Logic.list_implies (helper_prems, concl)))
   5.169 -                (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct)
   5.170 +                (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
   5.171 +                  dtor_unfold_thms set_mapss j set_induct)
   5.172                |> Thm.close_derivation
   5.173                |> split_conj_thm)
   5.174              mk_helper_ind_concls ls dtor_Jset_induct_thms
   5.175              |> transpose;
   5.176          in
   5.177 -          mk_rel_coinduct_tac in_rels in_Jrels
   5.178 +          mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels
   5.179              helper_ind_thmss helper_coind1_thms helper_coind2_thms
   5.180          end;
   5.181  
   5.182 @@ -2674,9 +2685,9 @@
   5.183          val map_id0_tacs =
   5.184            map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
   5.185          val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
   5.186 -        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
   5.187 -        val set_nat_tacss =
   5.188 -          map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
   5.189 +        val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms;
   5.190 +        val set_map0_tacss =
   5.191 +          map2 (map2 (fn def => fn col => fn ctxt =>
   5.192                unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col))
   5.193              hset_defss (transpose col_natural_thmss);
   5.194  
   5.195 @@ -2687,7 +2698,7 @@
   5.196          val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
   5.197  
   5.198          val set_bd_tacss =
   5.199 -          map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
   5.200 +          map3 (fn Cinf => map2 (fn def => fn col => fn ctxt =>
   5.201              unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col))
   5.202            Jbd_Cinfinites hset_defss (transpose col_bd_thmss);
   5.203  
   5.204 @@ -2695,11 +2706,11 @@
   5.205  
   5.206          val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
   5.207  
   5.208 -        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
   5.209 +        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
   5.210            bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
   5.211  
   5.212 -        fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN
   5.213 -          mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt;
   5.214 +        fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN
   5.215 +          mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
   5.216  
   5.217          val (Jbnfs, lthy) =
   5.218            fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
   5.219 @@ -2750,8 +2761,8 @@
   5.220            (if m = 0 then map HOLogic.eq_const Ts
   5.221              else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
   5.222            (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
   5.223 -          (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
   5.224 -            dtor_unfold_thms)
   5.225 +          (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
   5.226 +            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
   5.227            lthy;
   5.228  
   5.229        val timer = time (timer "relator coinduction");
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
     6.3 @@ -9,41 +9,35 @@
     6.4  
     6.5  signature BNF_GFP_TACTICS =
     6.6  sig
     6.7 -  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
     6.8 -    thm list list -> tactic
     6.9 -  val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
    6.10 -    {prems: 'a, context: Proof.context} -> tactic
    6.11 +  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list list ->
    6.12 +    tactic
    6.13 +  val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
    6.14    val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    6.15 -  val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    6.16 +  val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
    6.17    val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
    6.18    val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    6.19      thm list list -> tactic
    6.20 -  val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
    6.21 -    {prems: 'a, context: Proof.context} -> tactic
    6.22 +  val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
    6.23    val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
    6.24      tactic
    6.25    val mk_coalg_set_tac: thm -> tactic
    6.26 -  val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
    6.27 -    {prems: 'a, context: Proof.context} -> tactic
    6.28 +  val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
    6.29    val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
    6.30      thm list list -> tactic
    6.31 -  val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
    6.32 -    {prems: 'a, context: Proof.context} -> tactic
    6.33 +  val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    6.34 +    thm list list -> tactic
    6.35    val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
    6.36 -  val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
    6.37 -    {prems: 'a, context: Proof.context} -> tactic
    6.38 -  val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
    6.39 -    tactic
    6.40 +  val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
    6.41 +  val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
    6.42    val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
    6.43    val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
    6.44    val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    6.45      thm -> thm -> thm list -> thm list -> thm list list -> tactic
    6.46 -  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    6.47 -    {prems: 'a, context: Proof.context} -> tactic
    6.48 +  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
    6.49    val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
    6.50 -  val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    6.51 -  val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
    6.52 -    {prems: 'a, context: Proof.context} -> tactic
    6.53 +  val mk_hset_minimal_tac: Proof.context -> int -> thm list -> thm -> tactic
    6.54 +  val mk_hset_rec_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
    6.55 +    tactic
    6.56    val mk_incl_lsbis_tac: int -> int -> thm -> tactic
    6.57    val mk_length_Lev'_tac: thm -> tactic
    6.58    val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
    6.59 @@ -52,17 +46,17 @@
    6.60      thm list list -> thm list list -> thm list list list -> tactic
    6.61    val mk_map_id0_tac: thm list -> thm -> thm -> tactic
    6.62    val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
    6.63 -  val mk_dtor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
    6.64 -  val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    6.65 -  val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
    6.66 -    thm list -> {prems: 'a, context: Proof.context} -> tactic
    6.67 +  val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
    6.68 +  val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
    6.69 +  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
    6.70 +    thm list -> thm list -> tactic
    6.71    val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
    6.72    val mk_mor_UNIV_tac: thm list -> thm -> tactic
    6.73 -  val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    6.74 -    thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
    6.75 -    thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    6.76 -    thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    6.77 -    {prems: 'a, context: Proof.context} -> tactic
    6.78 +  val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
    6.79 +    thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
    6.80 +    thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
    6.81 +    thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
    6.82 +    thm list -> thm list -> tactic
    6.83    val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
    6.84    val mk_mor_elim_tac: thm -> tactic
    6.85    val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
    6.86 @@ -75,12 +69,12 @@
    6.87    val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
    6.88    val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    6.89      thm list -> thm list -> thm -> thm list -> tactic
    6.90 -  val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
    6.91 -    {prems: thm list, context: Proof.context} -> tactic
    6.92 -  val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
    6.93 -    thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    6.94 -  val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
    6.95 -    {prems: 'a, context: Proof.context} -> tactic
    6.96 +  val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
    6.97 +    thm list -> thm list -> tactic
    6.98 +  val mk_rel_coinduct_coind_tac: Proof.context -> int -> thm -> int list -> thm list -> thm list ->
    6.99 +    thm list -> thm list list -> thm list -> thm list -> tactic
   6.100 +  val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
   6.101 +    int -> thm -> tactic
   6.102    val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   6.103    val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
   6.104    val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
   6.105 @@ -96,9 +90,8 @@
   6.106    val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
   6.107      thm list -> thm list -> thm list list -> thm list list -> tactic
   6.108    val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   6.109 -  val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
   6.110 -    {prems: thm list, context: Proof.context} -> tactic
   6.111 -  val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> Proof.context -> tactic
   6.112 +  val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   6.113 +  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
   6.114    val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic
   6.115  end;
   6.116  
   6.117 @@ -191,7 +184,7 @@
   6.118        mk_UnIN n i] @
   6.119      [etac @{thm UN_I}, atac]) 1;
   6.120  
   6.121 -fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
   6.122 +fun mk_hset_rec_minimal_tac ctxt m cts rec_0s rec_Sucs =
   6.123    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   6.124      REPEAT_DETERM o rtac allI,
   6.125      CONJ_WRAP' (fn thm => EVERY'
   6.126 @@ -206,7 +199,7 @@
   6.127              rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
   6.128        rec_Sucs] 1;
   6.129  
   6.130 -fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
   6.131 +fun mk_hset_minimal_tac ctxt n hset_defs hset_rec_minimal =
   6.132    (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
   6.133      rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
   6.134      EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
   6.135 @@ -319,8 +312,7 @@
   6.136          REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
   6.137          etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
   6.138  
   6.139 -fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
   6.140 -  {context = ctxt, prems = _} =
   6.141 +fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
   6.142    unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
   6.143    EVERY' [rtac conjI,
   6.144      CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
   6.145 @@ -329,7 +321,7 @@
   6.146          etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
   6.147      (coalg_ins ~~ morEs)] 1;
   6.148  
   6.149 -fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
   6.150 +fun mk_bis_Union_tac ctxt bis_def in_monos =
   6.151    let
   6.152      val n = length in_monos;
   6.153      val ks = 1 upto n;
   6.154 @@ -377,7 +369,7 @@
   6.155      rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
   6.156      etac @{thm relcompI}, atac] 1;
   6.157  
   6.158 -fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} =
   6.159 +fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
   6.160    let
   6.161      val n = length strT_defs;
   6.162      val ks = 1 upto n;
   6.163 @@ -661,10 +653,10 @@
   6.164        ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
   6.165    end;
   6.166  
   6.167 -fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   6.168 +fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   6.169    to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   6.170    prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
   6.171 -  map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
   6.172 +  map_comp_ids map_cong0s map_arg_congs =
   6.173    let
   6.174      val n = length beh_defs;
   6.175      val ks = 1 upto n;
   6.176 @@ -865,8 +857,7 @@
   6.177          rtac congruent_str_final, atac, rtac o_apply])
   6.178      (equiv_LSBISs ~~ congruent_str_finals)] 1;
   6.179  
   6.180 -fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
   6.181 -  {context = ctxt, prems = _} =
   6.182 +fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
   6.183    unfold_thms_tac ctxt defs THEN
   6.184    EVERY' [rtac conjI,
   6.185      CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
   6.186 @@ -878,7 +869,7 @@
   6.187          Abs_inverses (drop m coalg_final_sets))])
   6.188      (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
   6.189  
   6.190 -fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
   6.191 +fun mk_mor_Abs_tac ctxt defs Abs_inverses =
   6.192    unfold_thms_tac ctxt defs THEN
   6.193    EVERY' [rtac conjI,
   6.194      CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
   6.195 @@ -926,21 +917,20 @@
   6.196        rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
   6.197        rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
   6.198  
   6.199 -fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
   6.200 -  {context = ctxt, prems = _} =
   6.201 +fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
   6.202    unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
   6.203      rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
   6.204      EVERY' (map (fn thm =>
   6.205        rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
   6.206      rtac sym, rtac id_apply] 1;
   6.207  
   6.208 -fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
   6.209 +fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
   6.210    unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
   6.211      rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
   6.212      REPEAT_DETERM_N m o rtac refl,
   6.213      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
   6.214  
   6.215 -fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
   6.216 +fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
   6.217    unfold_thms_tac ctxt
   6.218      (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
   6.219    etac unfold_unique_mor 1;
   6.220 @@ -1052,13 +1042,12 @@
   6.221             rtac conjI, rtac refl, rtac refl]) ks]) 1
   6.222    end
   6.223  
   6.224 -fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
   6.225 +fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
   6.226    rtac unfold_unique 1 THEN
   6.227    unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
   6.228    ALLGOALS (etac sym);
   6.229  
   6.230 -fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
   6.231 -  {context = ctxt, prems = _} =
   6.232 +fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
   6.233    let
   6.234      val n = length dtor_maps;
   6.235    in
   6.236 @@ -1114,7 +1103,7 @@
   6.237      end)
   6.238    rel_Jrels rel_OOs) 1;
   6.239  
   6.240 -fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits ctxt =
   6.241 +fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
   6.242    ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   6.243    REPEAT_DETERM (atac 1 ORELSE
   6.244      EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
   6.245 @@ -1128,7 +1117,7 @@
   6.246            EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
   6.247              K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   6.248  
   6.249 -fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   6.250 +fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
   6.251    rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
   6.252    unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   6.253    ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
   6.254 @@ -1200,8 +1189,8 @@
   6.255      EVERY' [rtac iffI, if_tac, only_if_tac] 1
   6.256    end;
   6.257  
   6.258 -fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
   6.259 -  dtor_unfolds dtor_maps {context = ctxt, prems = _} =
   6.260 +fun mk_rel_coinduct_coind_tac ctxt m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
   6.261 +  dtor_unfolds dtor_maps =
   6.262    let val n = length ks;
   6.263    in
   6.264      EVERY' [DETERM o rtac coinduct,
   6.265 @@ -1234,7 +1223,7 @@
   6.266  
   6.267  val split_id_unfolds = @{thms prod.cases image_id id_apply};
   6.268  
   6.269 -fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} =
   6.270 +fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   6.271    let val n = length ks;
   6.272    in
   6.273      rtac set_induct 1 THEN
   6.274 @@ -1258,8 +1247,7 @@
   6.275      unfolds set_map0ss ks) 1
   6.276    end;
   6.277  
   6.278 -fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
   6.279 -  {context = ctxt, prems = CIHs} =
   6.280 +fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
   6.281    let val n = length in_rels;
   6.282    in
   6.283      Method.insert_tac CIHs 1 THEN
   6.284 @@ -1284,7 +1272,7 @@
   6.285      (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
   6.286    end;
   6.287  
   6.288 -fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
   6.289 +fun mk_unfold_transfer_tac ctxt m rel_coinduct map_transfers unfolds =
   6.290    let
   6.291      val n = length map_transfers;
   6.292    in
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jan 30 22:55:52 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 31 10:02:36 2014 +0100
     7.3 @@ -877,7 +877,7 @@
     7.4      val alg_select_thm = Goal.prove_sorry lthy [] []
     7.5        (HOLogic.mk_Trueprop (mk_Ball II
     7.6          (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
     7.7 -      (mk_alg_select_tac Abs_IIT_inverse_thm)
     7.8 +      (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
     7.9        |> Thm.close_derivation;
    7.10  
    7.11      val mor_select_thm =
    7.12 @@ -904,8 +904,9 @@
    7.13            (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
    7.14          val ex_mor = Goal.prove_sorry lthy [] []
    7.15            (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
    7.16 -          (mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
    7.17 -            card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
    7.18 +          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
    7.19 +            ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
    7.20 +            mor_incl_min_alg_thm)
    7.21            |> Thm.close_derivation;
    7.22  
    7.23          val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
    7.24 @@ -1062,7 +1063,8 @@
    7.25          val mor_Rep =
    7.26            Goal.prove_sorry lthy [] []
    7.27              (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
    7.28 -            (mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps)
    7.29 +            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
    7.30 +              inver_Reps)
    7.31            |> Thm.close_derivation;
    7.32  
    7.33          val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
    7.34 @@ -1292,7 +1294,8 @@
    7.35          val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
    7.36        in
    7.37          map2 (fn goal => fn foldx =>
    7.38 -          Goal.prove_sorry lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
    7.39 +          Goal.prove_sorry lthy [] [] goal
    7.40 +            (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
    7.41            |> Thm.close_derivation)
    7.42          goals ctor_fold_thms
    7.43        end;
    7.44 @@ -1306,7 +1309,8 @@
    7.45        in
    7.46          Goal.prove_sorry lthy [] []
    7.47            (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
    7.48 -          (mk_rec_unique_mor_tac rec_defs fst_rec_pair_thms fold_unique_mor_thm)
    7.49 +          (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
    7.50 +            fold_unique_mor_thm)
    7.51            |> Thm.close_derivation
    7.52        end;
    7.53  
    7.54 @@ -1389,7 +1393,8 @@
    7.55        in
    7.56          (singleton (Proof_Context.export names_lthy lthy)
    7.57            (Goal.prove_sorry lthy [] [] goal
    7.58 -            (mk_ctor_induct2_tac cTs cts ctor_induct_thm weak_ctor_induct_thms))
    7.59 +            (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
    7.60 +              weak_ctor_induct_thms))
    7.61            |> Thm.close_derivation,
    7.62          rev (Term.add_tfrees goal []))
    7.63        end;
    7.64 @@ -1551,7 +1556,7 @@
    7.65              val unique = Goal.prove_sorry lthy [] []
    7.66                (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
    7.67                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
    7.68 -                mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps ctxt)
    7.69 +                mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
    7.70                |> Thm.close_derivation;
    7.71            in
    7.72              `split_conj_thm unique
    7.73 @@ -1626,11 +1631,12 @@
    7.74                    (map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
    7.75                    fs Isetss_by_range Isetss_by_range';
    7.76  
    7.77 -            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_Imap_thms;
    7.78 +            fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
    7.79              val thms =
    7.80                map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
    7.81                  singleton (Proof_Context.export names_lthy lthy)
    7.82 -                  (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
    7.83 +                  (Goal.prove_sorry lthy [] [] goal
    7.84 +                    (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
    7.85                  |> Thm.close_derivation)
    7.86                goals csetss ctor_Iset_thmss inducts ls;
    7.87            in
    7.88 @@ -1653,13 +1659,13 @@
    7.89                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    7.90                    (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
    7.91  
    7.92 -            fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
    7.93 +            fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sum_Cinfinite set_bd_sumss;
    7.94              val thms =
    7.95                map4 (fn goal => fn ctor_sets => fn induct => fn i =>
    7.96                  singleton (Proof_Context.export names_lthy lthy)
    7.97                    (Goal.prove_sorry lthy [] [] goal
    7.98                      (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
    7.99 -                      mk_tac induct ctor_sets i ctxt))
   7.100 +                      mk_tac ctxt induct ctor_sets i))
   7.101                  |> Thm.close_derivation)
   7.102                goals ctor_Iset_thmss inducts ls;
   7.103            in
   7.104 @@ -1689,7 +1695,8 @@
   7.105  
   7.106              val thm = singleton (Proof_Context.export names_lthy lthy)
   7.107                (Goal.prove_sorry lthy [] [] goal
   7.108 -              (mk_mcong_tac (rtac induct) set_Iset_thmsss map_cong0s ctor_Imap_thms))
   7.109 +              (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
   7.110 +                map_cong0s ctor_Imap_thms))
   7.111                |> Thm.close_derivation;
   7.112            in
   7.113              split_conj_thm thm
   7.114 @@ -1746,8 +1753,8 @@
   7.115            in
   7.116              singleton (Proof_Context.export names_lthy lthy)
   7.117                (Goal.prove_sorry lthy [] [] goal
   7.118 -                (mk_le_rel_OO_tac m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strongs
   7.119 -                  rel_OOs))
   7.120 +                (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
   7.121 +                  ctor_Irel_thms rel_mono_strongs rel_OOs))
   7.122                |> Thm.close_derivation
   7.123            end;
   7.124  
   7.125 @@ -1756,11 +1763,11 @@
   7.126          val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_Imap_unique_thms;
   7.127          val map_comp0_tacs =
   7.128            map2 (K oo mk_map_comp0_tac map_comps ctor_Imap_thms) ctor_Imap_unique_thms ks;
   7.129 -        val map_cong0_tacs = map (mk_map_cong0_tac m) Imap_cong0_thms;
   7.130 +        val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms;
   7.131          val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss);
   7.132 -        val bd_co_tacs = replicate n (fn {context = ctxt, prems = _} =>
   7.133 +        val bd_co_tacs = replicate n (fn ctxt =>
   7.134            unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders);
   7.135 -        val bd_cinf_tacs = replicate n (fn {context = ctxt, prems = _} =>
   7.136 +        val bd_cinf_tacs = replicate n (fn ctxt =>
   7.137            unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1);
   7.138          val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss);
   7.139          val le_rel_OO_tacs = map (fn i =>
   7.140 @@ -1771,7 +1778,7 @@
   7.141          val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
   7.142            bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
   7.143  
   7.144 -        fun wit_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Iwit_defss) THEN
   7.145 +        fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
   7.146            mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
   7.147  
   7.148          val (Ibnfs, lthy) =
   7.149 @@ -1816,13 +1823,15 @@
   7.150          else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
   7.151        val Irel_induct_thm =
   7.152          mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
   7.153 -          (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strongs) lthy;
   7.154 +          (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
   7.155 +             ctor_Irel_thms rel_mono_strongs) lthy;
   7.156  
   7.157        val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
   7.158        val ctor_fold_transfer_thms =
   7.159          mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
   7.160            (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
   7.161 -          (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
   7.162 +          (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
   7.163 +            (map map_transfer_of_bnf bnfs) ctor_fold_thms)
   7.164            lthy;
   7.165  
   7.166        val timer = time (timer "relator induction");
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
     8.3 @@ -11,7 +11,7 @@
     8.4    val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
     8.5      thm list -> tactic
     8.6    val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
     8.7 -  val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
     8.8 +  val mk_alg_select_tac: Proof.context -> thm -> tactic
     8.9    val mk_alg_set_tac: thm -> tactic
    8.10    val mk_bd_card_order_tac: thm list -> tactic
    8.11    val mk_bd_limit_tac: int -> thm -> tactic
    8.12 @@ -20,39 +20,37 @@
    8.13    val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
    8.14    val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
    8.15      thm list -> thm list -> thm list -> tactic
    8.16 -  val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
    8.17 -    {prems: 'a, context: Proof.context} -> tactic
    8.18 +  val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
    8.19 +    thm list -> tactic
    8.20    val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
    8.21    val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    8.22      thm -> thm -> thm list -> thm list -> thm list list -> tactic
    8.23    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    8.24    val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
    8.25 -  val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    8.26 -    {prems: 'a, context: Proof.context} -> tactic
    8.27 +  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    8.28 +    tactic
    8.29    val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
    8.30    val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    8.31      thm list -> tactic
    8.32    val mk_iso_alt_tac: thm list -> thm -> tactic
    8.33    val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    8.34 -  val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
    8.35 -    {prems: thm list, context: Proof.context} -> tactic
    8.36 +  val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    8.37    val mk_least_min_alg_tac: thm -> thm -> tactic
    8.38 -  val mk_le_rel_OO_tac: int -> thm -> thm list -> thm list -> thm list -> thm list ->
    8.39 -    {prems: 'a, context: Proof.context} -> tactic
    8.40 +  val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    8.41 +    thm list -> tactic
    8.42    val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
    8.43    val mk_map_id0_tac: thm list -> thm -> tactic
    8.44    val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
    8.45 -  val mk_ctor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
    8.46 -  val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
    8.47 -    {prems: 'a, context: Proof.context} -> tactic
    8.48 +  val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
    8.49 +  val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
    8.50 +    thm list -> tactic
    8.51    val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
    8.52      thm -> thm -> thm -> thm -> thm -> tactic
    8.53    val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
    8.54    val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
    8.55    val mk_min_algs_tac: thm -> thm list -> tactic
    8.56    val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
    8.57 -  val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
    8.58 -    {prems: 'a, context: Proof.context} -> tactic
    8.59 +  val mk_mor_Rep_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> thm list -> tactic
    8.60    val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
    8.61    val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
    8.62    val mk_mor_convol_tac: 'a list -> thm -> tactic
    8.63 @@ -63,15 +61,14 @@
    8.64    val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
    8.65      thm list -> tactic
    8.66    val mk_mor_str_tac: 'a list -> thm -> tactic
    8.67 -  val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
    8.68 -    {prems: thm list, context: Proof.context} -> tactic
    8.69 -  val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    8.70 -  val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
    8.71 -    tactic
    8.72 -  val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
    8.73 -    Proof.context -> tactic
    8.74 -  val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
    8.75 -    thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
    8.76 +  val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
    8.77 +    thm list -> tactic
    8.78 +  val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
    8.79 +  val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
    8.80 +  val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list ->
    8.81 +    int -> tactic
    8.82 +  val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
    8.83 +    cterm list -> thm list -> int -> tactic
    8.84    val mk_set_map0_tac: thm -> tactic
    8.85    val mk_set_tac: thm -> tactic
    8.86    val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
    8.87 @@ -385,7 +382,7 @@
    8.88    EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
    8.89      REPEAT_DETERM o etac conjE, atac] 1;
    8.90  
    8.91 -fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
    8.92 +fun mk_alg_select_tac ctxt Abs_inverse =
    8.93    EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
    8.94    unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
    8.95  
    8.96 @@ -410,8 +407,8 @@
    8.97      stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
    8.98    end;
    8.99  
   8.100 -fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
   8.101 -    mor_comp mor_select mor_incl_min_alg {context = ctxt, prems = _} =
   8.102 +fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
   8.103 +    mor_comp mor_select mor_incl_min_alg =
   8.104    let
   8.105      val n = length card_of_min_algs;
   8.106      val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso},
   8.107 @@ -486,7 +483,7 @@
   8.108      CONJ_WRAP' mk_induct_tac least_min_algs 1
   8.109    end;
   8.110  
   8.111 -fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
   8.112 +fun mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss inver_Reps =
   8.113    (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   8.114    EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   8.115    EVERY' (map rtac inver_Abss) THEN'
   8.116 @@ -522,13 +519,13 @@
   8.117        ctor_o_folds),
   8.118      rtac sym, rtac id_apply] 1;
   8.119  
   8.120 -fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
   8.121 +fun mk_rec_tac ctxt rec_defs foldx fst_recs =
   8.122    unfold_thms_tac ctxt
   8.123      (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   8.124    EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
   8.125      rtac @{thm snd_convol'}] 1;
   8.126  
   8.127 -fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} =
   8.128 +fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor =
   8.129    unfold_thms_tac ctxt
   8.130      (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
   8.131    etac fold_unique_mor 1;
   8.132 @@ -558,7 +555,7 @@
   8.133      DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
   8.134    end;
   8.135  
   8.136 -fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} =
   8.137 +fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts =
   8.138    let
   8.139      val n = length weak_ctor_inducts;
   8.140      val ks = 1 upto n;
   8.141 @@ -583,7 +580,7 @@
   8.142      REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
   8.143      rtac sym, rtac o_apply] 1;
   8.144  
   8.145 -fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
   8.146 +fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
   8.147    rtac fold_unique 1 THEN
   8.148    unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   8.149    ALLGOALS atac;
   8.150 @@ -603,8 +600,7 @@
   8.151        EVERY' (map mk_UN set_maps)] 1
   8.152    end;
   8.153  
   8.154 -fun mk_set_nat_tac m induct_tac set_mapss
   8.155 -    ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
   8.156 +fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i =
   8.157    let
   8.158      val n = length ctor_maps;
   8.159  
   8.160 @@ -623,7 +619,7 @@
   8.161      (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   8.162    end;
   8.163  
   8.164 -fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i ctxt =
   8.165 +fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
   8.166    let
   8.167      val n = length ctor_sets;
   8.168  
   8.169 @@ -639,7 +635,7 @@
   8.170      (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   8.171    end;
   8.172  
   8.173 -fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
   8.174 +fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
   8.175    let
   8.176      fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
   8.177  
   8.178 @@ -657,8 +653,7 @@
   8.179      (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   8.180    end;
   8.181  
   8.182 -fun mk_le_rel_OO_tac m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs 
   8.183 -    {context = ctxt, prems = _} =
   8.184 +fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs =
   8.185    EVERY' (rtac induct ::
   8.186    map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
   8.187      EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
   8.188 @@ -779,7 +774,7 @@
   8.189      EVERY' [rtac iffI, if_tac, only_if_tac] 1
   8.190    end;
   8.191  
   8.192 -fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
   8.193 +fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
   8.194    let val n = length ks;
   8.195    in
   8.196      unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
   8.197 @@ -794,7 +789,7 @@
   8.198        IHs ctor_rels rel_mono_strongs)] 1
   8.199    end;
   8.200  
   8.201 -fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
   8.202 +fun mk_fold_transfer_tac ctxt m rel_induct map_transfers folds =
   8.203    let
   8.204      val n = length map_transfers;
   8.205    in
     9.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
     9.3 @@ -21,11 +21,10 @@
     9.4    val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
     9.5    val mk_Abs_inj_thm: thm -> thm
     9.6  
     9.7 -  val mk_ctor_or_dtor_rel_tac:
     9.8 -    thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
     9.9 +  val mk_ctor_or_dtor_rel_tac: Proof.context -> thm -> thm list -> thm list -> thm -> tactic
    9.10  
    9.11    val mk_map_comp_id_tac: thm -> tactic
    9.12 -  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
    9.13 +  val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic
    9.14    val mk_map_cong0L_tac: int -> thm -> thm -> tactic
    9.15  end;
    9.16  
    9.17 @@ -85,7 +84,7 @@
    9.18      gen_tac
    9.19    end;
    9.20  
    9.21 -fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    9.22 +fun mk_ctor_or_dtor_rel_tac ctxt srel_def IJrel_defs IJsrel_defs dtor_srel =
    9.23    unfold_thms_tac ctxt IJrel_defs THEN
    9.24    rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    9.25      @{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
    9.26 @@ -97,7 +96,7 @@
    9.27  fun mk_map_comp_id_tac map_comp0 =
    9.28    (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;
    9.29  
    9.30 -fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
    9.31 +fun mk_map_cong0_tac ctxt m map_cong0 =
    9.32    EVERY' [rtac mp, rtac map_cong0,
    9.33      CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
    9.34