# HG changeset patch
# User nipkow
# Date 869736012 -7200
# Node ID 7544c866315c9c33a0d004629c6f65680d7ae210
# Parent  5ec1589eac1b015d83334c44ce393bb3bcff2716
Deleted comment.

diff -r 5ec1589eac1b -r 7544c866315c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Jul 24 11:13:12 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Jul 24 11:20:12 1997 +0200
@@ -103,7 +103,7 @@
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    "((~P) = (~Q)) = (P=Q)",
    "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
-   "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*)
+   "(? x. x=t & P(x)) = P(t)",
    "(! x. t=x --> P(x)) = P(t)" ];
 
 (*Add congruence rules for = (instead of ==) *)