src/Pure/raw_simplifier.ML
changeset 46707 1427dcc7c9a6
parent 46465 5ba52c337cd0
child 47239 0b1829860149
     1.1 --- a/src/Pure/raw_simplifier.ML	Mon Feb 27 15:39:47 2012 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Feb 27 15:42:07 2012 +0100
     1.3 @@ -1309,9 +1309,7 @@
     1.4        (global_context (Thm.theory_of_thm st) ss) i st
     1.5    end;
     1.6  
     1.7 -(*Prunes all redundant parameters from the proof state by rewriting.
     1.8 -  DOES NOT rewrite main goal, where quantification over an unused bound
     1.9 -    variable is sometimes done to avoid the need for cut_facts_tac.*)
    1.10 +(*Prunes all redundant parameters from the proof state by rewriting.*)
    1.11  val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
    1.12  
    1.13