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 =