# 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;