eliminated odd comment from distant past;
authorwenzelm
Mon Feb 27 15:42:07 2012 +0100 (2012-02-27)
changeset 467071427dcc7c9a6
parent 46706 877d57975427
child 46708 b138dee7bed3
eliminated odd comment from distant past;
src/Pure/raw_simplifier.ML
     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