# HG changeset patch
# User paulson
# Date 844073987 -7200
# Node ID 8de7a0ab463bed80f59f0919a67a61513af0e1e6
# Parent  33b4c1624e2606670c0141219081b96549881095
prune_params_tac no longer rewrites main goal

diff -r 33b4c1624e26 -r 8de7a0ab463b src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Sep 26 17:34:36 1996 +0200
+++ b/src/Pure/tactic.ML	Mon Sep 30 10:59:47 1996 +0200
@@ -518,8 +518,10 @@
       else all_tac
   end;
 
-(*Prunes all redundant parameters from the proof state by rewriting*)
-val prune_params_tac = rewrite_tac [triv_forall_equality];
+(*Prunes all redundant parameters from the proof state by rewriting.
+  DOES NOT rewrite main goal, where quantification over an unused bound
+    variable is sometimes done to avoid the need for cut_facts_tac.*)
+val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
 
 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   right to left if n is positive, and from left to right if n is negative.*)