commented

--- a/src/Pure/pure_thy.ML	Mon Apr 26 09:14:14 2004 +0200
+++ b/src/Pure/pure_thy.ML	Mon Apr 26 11:15:56 2004 +0200
@@ -516,6 +516,11 @@
 
 (*** the ProtoPure theory ***)
 
+
+(*It might make sense to restrict the polymorphism of the constant "==" to
+  sort logic, instead of the universal sort, {}.  Unfortunately, this change
+  causes HOL/Import/shuffler.ML to fail.*)
+
 val proto_pure =
   Theory.pre_pure
   |> Library.apply [TheoremsData.init, TheoryManagementData.init, Proofterm.init]