prune_params_tac no longer rewrites main goal
authorpaulson
Mon Sep 30 10:59:47 1996 +0200 (1996-09-30)
changeset 20438de7a0ab463b
parent 2042 33b4c1624e26
child 2044 e8d52d05530a
prune_params_tac no longer rewrites main goal
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Sep 26 17:34:36 1996 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Sep 30 10:59:47 1996 +0200
     1.3 @@ -518,8 +518,10 @@
     1.4        else all_tac
     1.5    end;
     1.6  
     1.7 -(*Prunes all redundant parameters from the proof state by rewriting*)
     1.8 -val prune_params_tac = rewrite_tac [triv_forall_equality];
     1.9 +(*Prunes all redundant parameters from the proof state by rewriting.
    1.10 +  DOES NOT rewrite main goal, where quantification over an unused bound
    1.11 +    variable is sometimes done to avoid the need for cut_facts_tac.*)
    1.12 +val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
    1.13  
    1.14  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
    1.15    right to left if n is positive, and from left to right if n is negative.*)