# HG changeset patch
# User wenzelm
# Date 978899711 -3600
# Node ID dd5fb02ff87208cc1b3ccd893a1102ebe64a9ae2
# Parent  2ccc84b8f5a01a011308606c83013a93e51884df
removed outdated comment;

diff -r 2ccc84b8f5a0 -r dd5fb02ff872 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Jan 07 21:34:45 2001 +0100
+++ b/src/Pure/drule.ML	Sun Jan 07 21:35:11 2001 +0100
@@ -590,10 +590,6 @@
 
 (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
   Rewrite rule for HHF normalization.
-
-  Note: the syntax of ProtoPure is insufficient to handle this
-  statement; storing it would be asking for trouble, e.g. when someone
-  tries to print the theory later.
 *)
 
 val norm_hhf_eq =