# HG changeset patch
# User wenzelm
# Date 1426762460 -3600
# Node ID 118f4995df8c92de4ae4ec185964a4f5491a1249
# Parent  a1c35e6fe735580a726fa0d8e76e3f5f07acf170
tuned comments;

diff -r a1c35e6fe735 -r 118f4995df8c src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Mar 19 11:13:54 2015 +0100
+++ b/src/Pure/tactic.ML	Thu Mar 19 11:54:20 2015 +0100
@@ -303,24 +303,27 @@
 fun rotate_tac 0 i = all_tac
   | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i);
 
-(*Rotates the given subgoal to be the last.*)
+(*Rotate the given subgoal to be the last.*)
 fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
 
-(*Rotates the given subgoal to be the first.*)
+(*Rotate the given subgoal to be the first.*)
 fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1);
 
-(* remove premises that do not satisfy p; fails if all prems satisfy p *)
-fun filter_prems_tac ctxt p =
-  let fun Then NONE tac = SOME tac
-        | Then (SOME tac) tac' = SOME(tac THEN' tac');
-      fun thins H (tac,n) =
-        if p H then (tac,n+1)
-        else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]),0);
-  in SUBGOAL(fn (subg,n) =>
-       let val Hs = Logic.strip_assums_hyp subg
-       in case fst(fold thins Hs (NONE,0)) of
-            NONE => no_tac | SOME tac => tac n
-       end)
+(*Remove premises that do not satisfy pred; fails if all prems satisfy pred.*)
+fun filter_prems_tac ctxt pred =
+  let
+    fun Then NONE tac = SOME tac
+      | Then (SOME tac) tac' = SOME (tac THEN' tac');
+    fun thins H (tac, n) =
+      if pred H then (tac, n + 1)
+      else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0);
+  in
+    SUBGOAL (fn (goal, i) =>
+      let val Hs = Logic.strip_assums_hyp goal in
+        (case fst (fold thins Hs (NONE, 0)) of
+          NONE => no_tac
+        | SOME tac => tac i)
+      end)
   end;
 
 end;