--- 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))