src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

       let
         val active :: actives' = actives;
         val dtor_corec_transfer' = cterm_instantiate_pos
           (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
       in
-        HEADGOAL Goal.conjunction_tac THEN
-        REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+        HEADGOAL Goal.conjunction_tac THEN REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
         unfold_thms_tac ctxt [corec_def] THEN
         HEADGOAL (etac (mk_rel_funDN_rotated (1 + length actives) dtor_corec_transfer')) THEN
         unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
       end;
 

     (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
      hyp_subst_tac ctxt ORELSE'
      SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o atac)))));
 
 fun mk_set_intros_tac ctxt sets =
-  TRYALL Goal.conjunction_tac THEN
-  unfold_thms_tac ctxt sets THEN
+  TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
   TRYALL (REPEAT o
     (resolve_tac ctxt @{thms UnI1 UnI2} ORELSE'
      eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac));
 
 fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors