# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID c81747d3e920caa685a211ec190d8581aa765d9f
# Parent  4e0f0f98be02da1c40050189d1d5a8d3fc388ce0
tuning

diff -r 4e0f0f98be02 -r c81747d3e920 src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -327,8 +327,7 @@
             val goal_weak =
               Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w));
           in
-            (Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-               mk_case_cong_tac ctxt exhaust_thm' case_thms),
+            (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
              Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
             |> pairself (singleton (Proof_Context.export names_lthy lthy))
           end;
@@ -350,8 +349,8 @@
                 (map3 mk_disjunct xctrs xss xfs)));
 
             val split_thm =
-              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms)
+              Skip_Proof.prove lthy [] [] goal
+                (fn _ => mk_split_tac exhaust_thm' case_thms inject_thms distinct_thms)
               |> singleton (Proof_Context.export names_lthy lthy)
             val split_asm_thm =
               Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
diff -r 4e0f0f98be02 -r c81747d3e920 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -7,14 +7,14 @@
 
 signature BNF_SUGAR_TACTICS =
 sig
-  val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_case_cong_tac: thm -> thm list -> tactic
   val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
   val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_disc_disjoint_tac: thm -> tactic
-  val mk_split_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
+  val mk_split_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic
 end;
 
@@ -67,13 +67,13 @@
        rtac case_thm]) case_thms sel_thmss)) 1
   end;
 
-fun mk_case_cong_tac ctxt exhaust' case_thms =
+fun mk_case_cong_tac exhaust' case_thms =
   (rtac exhaust' THEN'
    EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
 
 val naked_ctxt = Proof_Context.init_global @{theory HOL};
 
-fun mk_split_tac ctxt exhaust' case_thms injects distincts =
+fun mk_split_tac exhaust' case_thms injects distincts =
   rtac exhaust' 1 THEN
   ALLGOALS (hyp_subst_tac THEN'
     simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts))) THEN