# HG changeset patch
# User blanchet
# Date 1380204657 -7200
# Node ID 7b43d22accc33d79d24de57606d1c17fe032bd73
# Parent  6d40f6e69686a7553b474d4ba52a5f6aef18f424
tuning

diff -r 6d40f6e69686 -r 7b43d22accc3 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:00:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:10:57 2013 +0200
@@ -734,7 +734,7 @@
     val (defs, exclss') =
       co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
 
-    fun prove_excl_tac (c, c', a) =
+    fun excl_tac (c, c', a) =
       if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy []))
       else if simple then SOME (K (auto_tac lthy))
       else NONE;
@@ -745,7 +745,7 @@
 *)
 
     val exclss'' = exclss' |> map (map (fn (idx, t) =>
-      (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
+      (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     val (obligation_idxss, obligationss) = exclss''
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))