# 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];