# HG changeset patch
# User wenzelm
# Date 1449931062 -3600
# Node ID a3793600cb935966439f8c4c5c2ec2715e3a1777
# Parent  6f47a66afcd36997b747e4cdc692b99020370bf6
tuned;

diff -r 6f47a66afcd3 -r a3793600cb93 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:35:31 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:37:42 2015 +0100
@@ -748,13 +748,12 @@
                 fun filter_test prems t =
                   if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE;
               in
-                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st2 st |>
-                 (if n_subgoals = 0 orelse null local_thins then I
-                  else
-                    Seq.map (Goal.restrict 1 n_subgoals)
-                    #> Seq.maps (ALLGOALS (fn i =>
-                        DETERM (filter_prems_tac' goal_ctxt prep_filter filter_test local_thins i)))
-                    #> Seq.map (Goal.unrestrict 1))
+                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st2 st
+                |> (n_subgoals > 0 andalso not (null local_thins)) ?
+                    (Seq.map (Goal.restrict 1 n_subgoals)
+                      #> Seq.maps (ALLGOALS (fn i =>
+                          DETERM (filter_prems_tac' goal_ctxt prep_filter filter_test local_thins i)))
+                      #> Seq.map (Goal.unrestrict 1))
                 |> Seq.map (fold Thm.weaken extra_thins)
               end;