--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 23:30:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Feb 06 00:03:12 2014 +0100
@@ -162,7 +162,7 @@
fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
let
val splits' =
- map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
+ map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits);
in
HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
prelude_tac ctxt [] (fun_ctr RS trans) THEN