# HG changeset patch
# User traytel
# Date 1391158956 -3600
# Node ID 5a54ed681ba26d6148b0718d0835cfae9f4c6708
# Parent  a823137bcd87caf2121aa81373b334c08116929f
less hermetic tactics

diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Library/bnf_decl.ML
--- a/src/HOL/Library/bnf_decl.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -72,7 +72,7 @@
       user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
       lthy;
 
-    fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
+    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
 
@@ -81,7 +81,8 @@
       ||> `Local_Theory.restore;
 
     fun mk_wit_thms set_maps =
-      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
+        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
       |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -198,7 +198,7 @@
           val single_set_bd_thmss =
             map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
         in
-          map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
+          map2 (fn set_alt => fn single_set_bds => fn ctxt =>
             mk_comp_set_bd_tac ctxt set_alt single_set_bds)
           set_alt_thms single_set_bd_thmss
         end;
@@ -251,7 +251,7 @@
       |> minimize_wits
       |> map (fn (frees, t) => fold absfree frees t);
 
-    fun wit_tac {context = ctxt, prems = _} =
+    fun wit_tac ctxt =
       mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
         (maps wit_thms_of_bnf inners);
 
@@ -301,10 +301,10 @@
       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
-    fun map_comp0_tac {context = ctxt, prems = _} =
+    fun map_comp0_tac ctxt =
       unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
         @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
-    fun map_cong0_tac {context = ctxt, prems = _} =
+    fun map_cong0_tac ctxt =
       mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
     val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
     fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
@@ -322,7 +322,7 @@
         Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
       end;
 
-    fun le_rel_OO_tac {context = ctxt, prems = _} =
+    fun le_rel_OO_tac ctxt =
       EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
       unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
 
@@ -393,10 +393,10 @@
     val bd = mk_bd_of_bnf Ds As bnf;
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
-    fun map_comp0_tac {context = ctxt, prems = _} =
+    fun map_comp0_tac ctxt =
       unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
         @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
-    fun map_cong0_tac {context = ctxt, prems = _} =
+    fun map_cong0_tac ctxt =
       rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
     val set_map0_tacs =
       if Config.get lthy quick_and_dirty then
@@ -478,7 +478,7 @@
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
-    fun map_cong0_tac {context = ctxt, prems = _} =
+    fun map_cong0_tac ctxt =
       rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
     val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf));
     fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
@@ -628,7 +628,7 @@
     val set_bds =
       map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
 
-    fun mk_tac thm {context = ctxt, prems = _} =
+    fun mk_tac thm ctxt =
       (rtac (unfold_all ctxt thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
 
@@ -640,7 +640,7 @@
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac {context = ctxt, prems = _} =
+    fun wit_tac ctxt =
       mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
 
     val (bnf', lthy') =
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -106,7 +106,7 @@
     binding -> binding -> binding list ->
     (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
     string * term list *
-    ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
+    ((Proof.context -> thm list -> tactic) option * term list list) *
     ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
     local_theory * thm list
 
@@ -123,8 +123,8 @@
         (typ list -> typ list -> typ list -> term))) * local_theory
 
   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
-    ({prems: thm list, context: Proof.context} -> tactic) list ->
-    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
+    (Proof.context -> tactic) list ->
+    (Proof.context -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
     (((((binding * typ) * term) * term list) * term) * term list) * term option ->
     local_theory -> bnf * local_theory
@@ -1021,7 +1021,7 @@
         map wit_goal (0 upto live - 1)
       end;
 
-    val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
+    fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
 
     val wit_goalss =
       (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
@@ -1132,7 +1132,7 @@
                 (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
           in
             Goal.prove_sorry lthy [] [] in_bd_goal
-              (mk_in_bd_tac live surj_imp_ordLeq_inst
+              (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt live surj_imp_ordLeq_inst
                 (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
                 (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
                 bd_Card_order bd_Cinfinite bd_Cnotzero)
@@ -1151,8 +1151,9 @@
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
-              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
-                (Lazy.force map_comp) (map Lazy.force set_map))
+              (fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
+                (#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
+                (map Lazy.force set_map))
             |> Thm.close_derivation
           end;
 
@@ -1203,8 +1204,9 @@
             val rhs = mk_conversep (Term.list_comb (rel, Rs));
             val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
             val le_thm = Goal.prove_sorry lthy [] [] le_goal
-              (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
-                (Lazy.force map_comp) (map Lazy.force set_map))
+              (fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
+                (Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
+                (map Lazy.force set_map))
               |> Thm.close_derivation
             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
           in
@@ -1218,8 +1220,8 @@
         fun mk_rel_OO () =
           Goal.prove_sorry lthy [] []
             (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
-            (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
-              (Lazy.force map_comp) (map Lazy.force set_map))
+            (fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
+              (#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
           |> Thm.close_derivation
           |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
 
@@ -1254,7 +1256,8 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
-              (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map))
+              (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+                (map Lazy.force set_map))
             |> Thm.close_derivation
           end;
 
@@ -1271,8 +1274,9 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
-              (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
-                (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp))
+              (fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
+                (Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
+                (Lazy.force map_comp))
             |> Thm.close_derivation
           end;
 
@@ -1308,22 +1312,22 @@
 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
   let
-    fun mk_wits_tac set_maps =
-      K (TRYALL Goal.conjunction_tac) THEN'
+    fun mk_wits_tac ctxt set_maps =
+      TRYALL Goal.conjunction_tac THEN
       (case triv_tac_opt of
-        SOME tac => tac set_maps
-      | NONE => fn {context = ctxt, prems} =>
-          unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems});
+        SOME tac => tac ctxt set_maps
+      | NONE => unfold_thms_tac ctxt one_step_defs THEN wit_tac ctxt);
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     fun mk_wit_thms set_maps =
-      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
+      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
+        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
         |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
   in
     map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
-      goals (map (fn tac => fn {context = ctxt, prems} =>
-        unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs)
+      goals (map (fn tac => fn {context = ctxt, prems = _} =>
+        unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
   end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
 
@@ -1332,7 +1336,7 @@
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     fun mk_triv_wit_thms tac set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
-        (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps)
+        (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
         |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -15,25 +15,20 @@
   val mk_in_mono_tac: int -> tactic
   val mk_set_map: thm -> thm
 
-  val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
+  val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
-  val mk_rel_OO_le_tac: thm list -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
+  val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
   val mk_rel_conversep_tac: thm -> thm -> tactic
-  val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
+  val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
   val mk_rel_mono_tac: thm list -> thm -> tactic
-  val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
 
-  val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
-    {prems: thm list, context: Proof.context} -> tactic
+  val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
 
-  val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm ->
-    thm -> {prems: thm list, context: Proof.context} -> tactic
+  val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
+    thm -> thm -> thm -> thm -> tactic
 
-  val mk_trivial_wit_tac: thm list -> thm list -> {prems: thm list, context: Proof.context} ->
-    tactic
+  val mk_trivial_wit_tac: Proof.context -> thm list -> thm list -> tactic
 end;
 
 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -67,8 +62,7 @@
     rtac set_map0) set_map0s) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
-  {context = ctxt, prems = _} =
+fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
   let
     val n = length set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
@@ -120,8 +114,7 @@
       rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
   end;
 
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
-  {context = ctxt, prems = _} =
+fun mk_rel_conversep_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
   let
     val n = length set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
@@ -146,8 +139,7 @@
     rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
     REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
 
-fun mk_rel_OO_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
-  {context = ctxt, prems = _} =
+fun mk_rel_OO_le_tac ctxt rel_OO_Grps rel_eq map_cong0 map_comp set_maps =
   let
     val n = length set_maps;
     fun in_tac nthO_in = rtac CollectI THEN'
@@ -183,7 +175,7 @@
         in_tac @{thm sndOp_in}] 1
   end;
 
-fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
+fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
   if null set_maps then atac 1
   else
     unfold_tac ctxt [in_rel] THEN
@@ -194,8 +186,7 @@
         (etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
       set_maps] 1;
 
-fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
-  {context = ctxt, prems = _} =
+fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =
   let
     val n = length set_maps;
     val in_tac = if n = 0 then rtac UNIV_I else
@@ -216,8 +207,8 @@
         REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
   end;
 
-fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
-  bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
+fun mk_in_bd_tac ctxt live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds
+  bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero =
   if live = 0 then
     rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
       ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
@@ -278,7 +269,7 @@
            map_comp RS sym, map_id])] 1
   end;
 
-fun mk_trivial_wit_tac wit_defs set_maps {context = ctxt, prems = _} =
+fun mk_trivial_wit_tac ctxt wit_defs set_maps =
   unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
     dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
 
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -696,7 +696,8 @@
             map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
               singleton (Proof_Context.export names_lthy lthy)
                 (Goal.prove_sorry lthy [] [] goal
-                  (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
+                  (fn {context = ctxt, prems = _} => mk_hset_rec_minimal_tac ctxt m cts hset_rec_0s
+                    hset_rec_Sucs))
               |> Thm.close_derivation)
             goals ctss hset_rec_0ss' hset_rec_Sucss'
           end;
@@ -711,7 +712,8 @@
       in
         map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
           Goal.prove_sorry lthy [] [] goal
-            (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
+            (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n hset_defs
+              hset_rec_minimal)
           |> Thm.close_derivation)
         goals hset_defss' hset_rec_minimal_thms
       end;
@@ -830,7 +832,8 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([coalg_prem, mor_prem], concl)))
-          (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
+          (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
+            morE_thms coalg_in_thms)
         |> Thm.close_derivation
       end;
 
@@ -852,7 +855,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
             (Logic.mk_implies (prem, concl)))
-          (mk_bis_Union_tac bis_def in_mono'_thms)
+          (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
         |> Thm.close_derivation
       end;
 
@@ -1193,7 +1196,8 @@
     val coalgT_thm =
       Goal.prove_sorry lthy [] []
         (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
-        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
+        (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
+          (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
       |> Thm.close_derivation;
 
     val timer = time (timer "Tree coalgebra");
@@ -1557,7 +1561,7 @@
       Goal.prove_sorry lthy [] []
         (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
           HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
-        (mk_mor_beh_tac m mor_def mor_cong_thm
+        (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
           beh_defs carT_defs strT_defs isNode_defs
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
           length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
@@ -1709,14 +1713,15 @@
         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
-            (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
-              map_comp_id_thms map_cong0L_thms)
+            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
+              Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
           |> Thm.close_derivation;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
-            (mk_mor_Abs_tac (mor_def :: dtor_defs) Abs_inverses)
+            (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
+              Abs_inverses)
           |> Thm.close_derivation;
       in
         (mor_Rep, mor_Abs)
@@ -1863,7 +1868,8 @@
       in
         map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
-            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
+            (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
+              map_cong0L unfold_o_dtor_thms)
           |> Thm.close_derivation)
           goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
       end;
@@ -1948,7 +1954,8 @@
       in
         map3 (fn goal => fn unfold => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
-            (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
+            (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
+              corec_Inl_sum_thms)
           |> Thm.close_derivation)
         goals dtor_unfold_thms map_cong0s
       end;
@@ -1963,7 +1970,8 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
-          (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm)
+          (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
+            corec_Inl_sum_thms unfold_unique_mor_thm)
           |> Thm.close_derivation
       end;
 
@@ -2278,7 +2286,8 @@
           in
             map2 (fn goal => fn induct =>
               Goal.prove_sorry lthy [] [] goal
-                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_mapss) wit_thms)
+                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
+                  (flat set_mapss) wit_thms)
               |> Thm.close_derivation)
             goals dtor_hset_induct_thms
             |> map split_conj_thm
@@ -2362,7 +2371,7 @@
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
                 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
-                  mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt)
+                  mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
               |> Thm.close_derivation
           end;
 
@@ -2444,7 +2453,8 @@
               map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 singleton (Proof_Context.export names_lthy lthy)
                   (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss))
+                    (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
+                      dtor_Jmap_thms set_mapss))
                 |> Thm.close_derivation)
               goals ctss hset_rec_0ss' hset_rec_Sucss';
           in
@@ -2586,7 +2596,7 @@
       val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
       val zip_setss = mk_Jsetss passiveABs |> transpose;
 
-      val Jrel_coinduct_tac =
+      fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
         let
           fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
             let
@@ -2611,13 +2621,13 @@
             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
               (map6 (mk_helper_coind_concl false)
               activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
-          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
-            map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms;
           fun mk_helper_coind_thms vars concl =
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
                 (Logic.list_implies (helper_prems, concl)))
-              helper_coind_tac
+              (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m
+                dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss
+                dtor_unfold_thms dtor_Jmap_thms)
             |> Thm.close_derivation
             |> split_conj_thm;
           val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
@@ -2641,13 +2651,14 @@
               Goal.prove_sorry lthy [] []
                 (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
                   (Logic.list_implies (helper_prems, concl)))
-                (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct)
+                (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
+                  dtor_unfold_thms set_mapss j set_induct)
               |> Thm.close_derivation
               |> split_conj_thm)
             mk_helper_ind_concls ls dtor_Jset_induct_thms
             |> transpose;
         in
-          mk_rel_coinduct_tac in_rels in_Jrels
+          mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels
             helper_ind_thmss helper_coind1_thms helper_coind2_thms
         end;
 
@@ -2674,9 +2685,9 @@
         val map_id0_tacs =
           map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
         val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
-        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
-        val set_nat_tacss =
-          map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+        val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms;
+        val set_map0_tacss =
+          map2 (map2 (fn def => fn col => fn ctxt =>
               unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col))
             hset_defss (transpose col_natural_thmss);
 
@@ -2687,7 +2698,7 @@
         val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
 
         val set_bd_tacss =
-          map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+          map3 (fn Cinf => map2 (fn def => fn col => fn ctxt =>
             unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col))
           Jbd_Cinfinites hset_defss (transpose col_bd_thmss);
 
@@ -2695,11 +2706,11 @@
 
         val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
 
-        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
+        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
-        fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN
-          mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt;
+        fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN
+          mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
 
         val (Jbnfs, lthy) =
           fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
@@ -2750,8 +2761,8 @@
           (if m = 0 then map HOLogic.eq_const Ts
             else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
           (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
-          (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
-            dtor_unfold_thms)
+          (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
+            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
           lthy;
 
       val timer = time (timer "relator coinduction");
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -9,41 +9,35 @@
 
 signature BNF_GFP_TACTICS =
 sig
-  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
-    thm list list -> tactic
-  val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list list ->
+    tactic
+  val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
   val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
-  val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
   val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
   val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
     thm list list -> tactic
-  val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
   val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
     tactic
   val mk_coalg_set_tac: thm -> tactic
-  val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
   val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
     thm list list -> tactic
-  val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
+    thm list list -> tactic
   val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
-  val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
-  val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
-    tactic
+  val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
+  val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
   val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
-  val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_hset_minimal_tac: Proof.context -> int -> thm list -> thm -> tactic
+  val mk_hset_rec_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
+    tactic
   val mk_incl_lsbis_tac: int -> int -> thm -> tactic
   val mk_length_Lev'_tac: thm -> tactic
   val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
@@ -52,17 +46,17 @@
     thm list list -> thm list list -> thm list list list -> tactic
   val mk_map_id0_tac: thm list -> thm -> thm -> tactic
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
-  val mk_dtor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
-  val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
-    thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
+  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
+    thm list -> thm list -> tactic
   val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
   val mk_mor_UNIV_tac: thm list -> thm -> tactic
-  val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
-    thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
-    thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
+    thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
+    thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
+    thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
+    thm list -> thm list -> tactic
   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
   val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
@@ -75,12 +69,12 @@
   val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
     thm list -> thm list -> thm -> thm list -> tactic
-  val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
-    thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
+    thm list -> thm list -> tactic
+  val mk_rel_coinduct_coind_tac: Proof.context -> int -> thm -> int list -> thm list -> thm list ->
+    thm list -> thm list list -> thm list -> thm list -> tactic
+  val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
+    int -> thm -> tactic
   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
   val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
@@ -96,9 +90,8 @@
   val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
     thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
-  val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
+  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
   val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic
 end;
 
@@ -191,7 +184,7 @@
       mk_UnIN n i] @
     [etac @{thm UN_I}, atac]) 1;
 
-fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
+fun mk_hset_rec_minimal_tac ctxt m cts rec_0s rec_Sucs =
   EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn thm => EVERY'
@@ -206,7 +199,7 @@
             rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
       rec_Sucs] 1;
 
-fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} =
+fun mk_hset_minimal_tac ctxt n hset_defs hset_rec_minimal =
   (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def,
     rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal,
     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
@@ -319,8 +312,7 @@
         REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
 
-fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
-  {context = ctxt, prems = _} =
+fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
   unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
@@ -329,7 +321,7 @@
         etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
     (coalg_ins ~~ morEs)] 1;
 
-fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
+fun mk_bis_Union_tac ctxt bis_def in_monos =
   let
     val n = length in_monos;
     val ks = 1 upto n;
@@ -377,7 +369,7 @@
     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
     etac @{thm relcompI}, atac] 1;
 
-fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} =
+fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
   let
     val n = length strT_defs;
     val ks = 1 upto n;
@@ -661,10 +653,10 @@
       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
   end;
 
-fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
+fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
-  map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
+  map_comp_ids map_cong0s map_arg_congs =
   let
     val n = length beh_defs;
     val ks = 1 upto n;
@@ -865,8 +857,7 @@
         rtac congruent_str_final, atac, rtac o_apply])
     (equiv_LSBISs ~~ congruent_str_finals)] 1;
 
-fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
-  {context = ctxt, prems = _} =
+fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
@@ -878,7 +869,7 @@
         Abs_inverses (drop m coalg_final_sets))])
     (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
 
-fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
+fun mk_mor_Abs_tac ctxt defs Abs_inverses =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
@@ -926,21 +917,20 @@
       rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
       rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
 
-fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
-  {context = ctxt, prems = _} =
+fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
   unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
     rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm =>
       rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
     rtac sym, rtac id_apply] 1;
 
-fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
+fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
   unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
     rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
-fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
+fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
   unfold_thms_tac ctxt
     (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
   etac unfold_unique_mor 1;
@@ -1052,13 +1042,12 @@
            rtac conjI, rtac refl, rtac refl]) ks]) 1
   end
 
-fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
+fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
   rtac unfold_unique 1 THEN
   unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
   ALLGOALS (etac sym);
 
-fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
-  {context = ctxt, prems = _} =
+fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
   let
     val n = length dtor_maps;
   in
@@ -1114,7 +1103,7 @@
     end)
   rel_Jrels rel_OOs) 1;
 
-fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits ctxt =
+fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
     EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
@@ -1128,7 +1117,7 @@
           EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
             K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
+fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
   rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
@@ -1200,8 +1189,8 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
-  dtor_unfolds dtor_maps {context = ctxt, prems = _} =
+fun mk_rel_coinduct_coind_tac ctxt m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
+  dtor_unfolds dtor_maps =
   let val n = length ks;
   in
     EVERY' [DETERM o rtac coinduct,
@@ -1234,7 +1223,7 @@
 
 val split_id_unfolds = @{thms prod.cases image_id id_apply};
 
-fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} =
+fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   let val n = length ks;
   in
     rtac set_induct 1 THEN
@@ -1258,8 +1247,7 @@
     unfolds set_map0ss ks) 1
   end;
 
-fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
-  {context = ctxt, prems = CIHs} =
+fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
   let val n = length in_rels;
   in
     Method.insert_tac CIHs 1 THEN
@@ -1284,7 +1272,7 @@
     (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
   end;
 
-fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
+fun mk_unfold_transfer_tac ctxt m rel_coinduct map_transfers unfolds =
   let
     val n = length map_transfers;
   in
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -877,7 +877,7 @@
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
         (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
-      (mk_alg_select_tac Abs_IIT_inverse_thm)
+      (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
       |> Thm.close_derivation;
 
     val mor_select_thm =
@@ -904,8 +904,9 @@
           (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
         val ex_mor = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
-          (mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
-            card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
+          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
+            ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
+            mor_incl_min_alg_thm)
           |> Thm.close_derivation;
 
         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
@@ -1062,7 +1063,8 @@
         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
-            (mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps)
+            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
+              inver_Reps)
           |> Thm.close_derivation;
 
         val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
@@ -1292,7 +1294,8 @@
         val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
       in
         map2 (fn goal => fn foldx =>
-          Goal.prove_sorry lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
+          Goal.prove_sorry lthy [] [] goal
+            (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
           |> Thm.close_derivation)
         goals ctor_fold_thms
       end;
@@ -1306,7 +1309,8 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
-          (mk_rec_unique_mor_tac rec_defs fst_rec_pair_thms fold_unique_mor_thm)
+          (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
+            fold_unique_mor_thm)
           |> Thm.close_derivation
       end;
 
@@ -1389,7 +1393,8 @@
       in
         (singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] goal
-            (mk_ctor_induct2_tac cTs cts ctor_induct_thm weak_ctor_induct_thms))
+            (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
+              weak_ctor_induct_thms))
           |> Thm.close_derivation,
         rev (Term.add_tfrees goal []))
       end;
@@ -1551,7 +1556,7 @@
             val unique = Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
-                mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps ctxt)
+                mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
               |> Thm.close_derivation;
           in
             `split_conj_thm unique
@@ -1626,11 +1631,12 @@
                   (map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
                   fs Isetss_by_range Isetss_by_range';
 
-            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_Imap_thms;
+            fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
             val thms =
               map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
                 singleton (Proof_Context.export names_lthy lthy)
-                  (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
+                  (Goal.prove_sorry lthy [] [] goal
+                    (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
                 |> Thm.close_derivation)
               goals csetss ctor_Iset_thmss inducts ls;
           in
@@ -1653,13 +1659,13 @@
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                   (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
 
-            fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
+            fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sum_Cinfinite set_bd_sumss;
             val thms =
               map4 (fn goal => fn ctor_sets => fn induct => fn i =>
                 singleton (Proof_Context.export names_lthy lthy)
                   (Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
-                      mk_tac induct ctor_sets i ctxt))
+                      mk_tac ctxt induct ctor_sets i))
                 |> Thm.close_derivation)
               goals ctor_Iset_thmss inducts ls;
           in
@@ -1689,7 +1695,8 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (mk_mcong_tac (rtac induct) set_Iset_thmsss map_cong0s ctor_Imap_thms))
+              (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
+                map_cong0s ctor_Imap_thms))
               |> Thm.close_derivation;
           in
             split_conj_thm thm
@@ -1746,8 +1753,8 @@
           in
             singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-                (mk_le_rel_OO_tac m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strongs
-                  rel_OOs))
+                (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
+                  ctor_Irel_thms rel_mono_strongs rel_OOs))
               |> Thm.close_derivation
           end;
 
@@ -1756,11 +1763,11 @@
         val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_Imap_unique_thms;
         val map_comp0_tacs =
           map2 (K oo mk_map_comp0_tac map_comps ctor_Imap_thms) ctor_Imap_unique_thms ks;
-        val map_cong0_tacs = map (mk_map_cong0_tac m) Imap_cong0_thms;
+        val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms;
         val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss);
-        val bd_co_tacs = replicate n (fn {context = ctxt, prems = _} =>
+        val bd_co_tacs = replicate n (fn ctxt =>
           unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders);
-        val bd_cinf_tacs = replicate n (fn {context = ctxt, prems = _} =>
+        val bd_cinf_tacs = replicate n (fn ctxt =>
           unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1);
         val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss);
         val le_rel_OO_tacs = map (fn i =>
@@ -1771,7 +1778,7 @@
         val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
-        fun wit_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Iwit_defss) THEN
+        fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
           mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
@@ -1816,13 +1823,15 @@
         else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
       val Irel_induct_thm =
         mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
-          (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strongs) lthy;
+          (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
+             ctor_Irel_thms rel_mono_strongs) lthy;
 
       val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
       val ctor_fold_transfer_thms =
         mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
           (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
-          (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
+          (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
+            (map map_transfer_of_bnf bnfs) ctor_fold_thms)
           lthy;
 
       val timer = time (timer "relator induction");
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -11,7 +11,7 @@
   val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
     thm list -> tactic
   val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
-  val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_alg_select_tac: Proof.context -> thm -> tactic
   val mk_alg_set_tac: thm -> tactic
   val mk_bd_card_order_tac: thm list -> tactic
   val mk_bd_limit_tac: int -> thm -> tactic
@@ -20,39 +20,37 @@
   val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
   val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
     thm list -> thm list -> thm list -> tactic
-  val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
+    thm list -> tactic
   val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
   val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
-  val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
+    tactic
   val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
   val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
     thm list -> tactic
   val mk_iso_alt_tac: thm list -> thm -> tactic
   val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
-  val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
+  val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
-  val mk_le_rel_OO_tac: int -> thm -> thm list -> thm list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_le_rel_OO_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+    thm list -> tactic
   val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
   val mk_map_id0_tac: thm list -> thm -> tactic
   val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
-  val mk_ctor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
-  val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_ctor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_mcong_tac: Proof.context -> (int -> tactic) -> thm list list list -> thm list ->
+    thm list -> tactic
   val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
     thm -> thm -> thm -> thm -> thm -> tactic
   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   val mk_min_algs_tac: thm -> thm list -> tactic
   val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
-  val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
-    {prems: 'a, context: Proof.context} -> tactic
+  val mk_mor_Rep_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
   val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
   val mk_mor_convol_tac: 'a list -> thm -> tactic
@@ -63,15 +61,14 @@
   val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
-  val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
-    tactic
-  val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
-    Proof.context -> tactic
-  val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
-    thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_induct_tac: Proof.context -> thm list -> int -> thm -> int list -> thm list ->
+    thm list -> tactic
+  val mk_rec_tac: Proof.context -> thm list -> thm -> thm list -> tactic
+  val mk_rec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
+  val mk_set_bd_tac: Proof.context -> int -> (int -> tactic) -> thm -> thm list list -> thm list ->
+    int -> tactic
+  val mk_set_nat_tac: Proof.context -> int -> (int -> tactic) -> thm list list -> thm list ->
+    cterm list -> thm list -> int -> tactic
   val mk_set_map0_tac: thm -> tactic
   val mk_set_tac: thm -> tactic
   val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
@@ -385,7 +382,7 @@
   EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
     REPEAT_DETERM o etac conjE, atac] 1;
 
-fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
+fun mk_alg_select_tac ctxt Abs_inverse =
   EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
   unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
 
@@ -410,8 +407,8 @@
     stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
   end;
 
-fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
-    mor_comp mor_select mor_incl_min_alg {context = ctxt, prems = _} =
+fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
+    mor_comp mor_select mor_incl_min_alg =
   let
     val n = length card_of_min_algs;
     val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso},
@@ -486,7 +483,7 @@
     CONJ_WRAP' mk_induct_tac least_min_algs 1
   end;
 
-fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
+fun mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss inver_Reps =
   (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   EVERY' (map rtac inver_Abss) THEN'
@@ -522,13 +519,13 @@
       ctor_o_folds),
     rtac sym, rtac id_apply] 1;
 
-fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
+fun mk_rec_tac ctxt rec_defs foldx fst_recs =
   unfold_thms_tac ctxt
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
-fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} =
+fun mk_rec_unique_mor_tac ctxt rec_defs fst_recs fold_unique_mor =
   unfold_thms_tac ctxt
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
   etac fold_unique_mor 1;
@@ -558,7 +555,7 @@
     DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1
   end;
 
-fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} =
+fun mk_ctor_induct2_tac ctxt cTs cts ctor_induct weak_ctor_inducts =
   let
     val n = length weak_ctor_inducts;
     val ks = 1 upto n;
@@ -583,7 +580,7 @@
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
     rtac sym, rtac o_apply] 1;
 
-fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
+fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps =
   rtac fold_unique 1 THEN
   unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   ALLGOALS atac;
@@ -603,8 +600,7 @@
       EVERY' (map mk_UN set_maps)] 1
   end;
 
-fun mk_set_nat_tac m induct_tac set_mapss
-    ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
+fun mk_set_nat_tac ctxt m induct_tac set_mapss ctor_maps csets ctor_sets i =
   let
     val n = length ctor_maps;
 
@@ -623,7 +619,7 @@
     (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   end;
 
-fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i ctxt =
+fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
   let
     val n = length ctor_sets;
 
@@ -639,7 +635,7 @@
     (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   end;
 
-fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
+fun mk_mcong_tac ctxt induct_tac set_setsss map_cong0s ctor_maps =
   let
     fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
 
@@ -657,8 +653,7 @@
     (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
-fun mk_le_rel_OO_tac m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs 
-    {context = ctxt, prems = _} =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs =
   EVERY' (rtac induct ::
   map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
     EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
@@ -779,7 +774,7 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
+fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
   let val n = length ks;
   in
     unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
@@ -794,7 +789,7 @@
       IHs ctor_rels rel_mono_strongs)] 1
   end;
 
-fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
+fun mk_fold_transfer_tac ctxt m rel_induct map_transfers folds =
   let
     val n = length map_transfers;
   in
diff -r a823137bcd87 -r 5a54ed681ba2 src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Thu Jan 30 22:55:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Jan 31 10:02:36 2014 +0100
@@ -21,11 +21,10 @@
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
-  val mk_ctor_or_dtor_rel_tac:
-    thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_ctor_or_dtor_rel_tac: Proof.context -> thm -> thm list -> thm list -> thm -> tactic
 
   val mk_map_comp_id_tac: thm -> tactic
-  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic
   val mk_map_cong0L_tac: int -> thm -> thm -> tactic
 end;
 
@@ -85,7 +84,7 @@
     gen_tac
   end;
 
-fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
+fun mk_ctor_or_dtor_rel_tac ctxt srel_def IJrel_defs IJsrel_defs dtor_srel =
   unfold_thms_tac ctxt IJrel_defs THEN
   rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
     @{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
@@ -97,7 +96,7 @@
 fun mk_map_comp_id_tac map_comp0 =
   (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;
 
-fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
+fun mk_map_cong0_tac ctxt m map_cong0 =
   EVERY' [rtac mp, rtac map_cong0,
     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;