# HG changeset patch
# User blanchet
# Date 1387552930 -3600
# Node ID 5bc637eb60c071133f0d455aadc62f854cd06a80
# Parent  47857a79bdad45a51408caca8eb22d335e3da465
tuning whitespace

diff -r 47857a79bdad -r 5bc637eb60c0 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Dec 20 14:27:07 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Dec 20 16:22:10 2013 +0100
@@ -166,8 +166,8 @@
 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
     discss selss =
   let val ks = 1 upto n in
-    EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac
-        meta_spec, dtac meta_mp, atac, rtac exhaust, K (HEADGOAL (inst_as_projs_tac ctxt)),
+    EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk,
+        dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (HEADGOAL (inst_as_projs_tac ctxt)),
         hyp_subst_tac ctxt] @
       map4 (fn k => fn ctr_def => fn discs => fn sels =>
         EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @