--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 24 18:10:56 2015 +0100
@@ -106,9 +106,7 @@
val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
fun mk_case_transfer_tac ctxt rel_cases cases =
- let
- val n = length (tl (Thm.prems_of rel_cases));
- in
+ let val n = length (tl (Thm.prems_of rel_cases)) in
REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
HEADGOAL (etac rel_cases) THEN
ALLGOALS (hyp_subst_tac ctxt) THEN