# HG changeset patch
# User paulson
# Date 837524907 -7200
# Node ID 37615e73f2d8667ee6c02491224883e9a9295fe0
# Parent  a1a41b4b02e72822a605092a0494eea6877cbeee
corrected comment

diff -r a1a41b4b02e7 -r 37615e73f2d8 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Tue Jul 16 15:47:07 1996 +0200
+++ b/src/HOL/indrule.ML	Tue Jul 16 15:48:27 1996 +0200
@@ -185,7 +185,7 @@
            rewrite_goals_tac all_defs  THEN
            simp_tac (mut_ss addsimps [Part_def]) 1  THEN
            IF_UNSOLVED (*simp_tac may have finished it off!*)
-             ((*simplify assumptions, but don't accept new rewrite rules!*)
+             ((*simplify assumptions*)
               full_simp_tac mut_ss 1  THEN
               (*unpackage and use "prem" in the corresponding place*)
               REPEAT (rtac impI 1)  THEN