# HG changeset patch
# User blanchet
# Date 1420437375 -3600
# Node ID d1def4b100edf5334eda68645ddd7843658bcf35
# Parent  8713bd81017d6bd49106eb8415b63734fc6dd3d7
tuning

diff -r 8713bd81017d -r d1def4b100ed src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Dec 19 11:18:23 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -467,10 +467,9 @@
   HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
     rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
-  unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
-    ((discs @ distincts) RL [eqTrueI, eqFalseI]) @
-    (rel_injects RL [eqTrueI]) @
-    (rel_distincts RL [eqFalseI])) THEN
+  unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @
+    @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ ((discs @ distincts) RL [eqTrueI, eqFalseI]) @
+    (rel_injects RL [eqTrueI]) @ (rel_distincts RL [eqFalseI])) THEN
   TRYALL (resolve_tac [TrueI, refl]);
 
 fun mk_sel_transfer_tac ctxt n sel_defs case_transfer =