# 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.*)