# HG changeset patch
# User wenzelm
# Date 1330353727 -3600
# Node ID 1427dcc7c9a6a733378533ad6e464fb477479d4d
# Parent  877d5797542766a7a57008d1bd9245b9842d2c14
eliminated odd comment from distant past;

diff -r 877d57975427 -r 1427dcc7c9a6 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Feb 27 15:39:47 2012 +0100
+++ b/src/Pure/raw_simplifier.ML	Mon Feb 27 15:42:07 2012 +0100
@@ -1309,9 +1309,7 @@
       (global_context (Thm.theory_of_thm st) ss) i st
   end;
 
-(*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.*)
+(*Prunes all redundant parameters from the proof state by rewriting.*)
 val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];