# HG changeset patch
# User paulson
# Date 1082970956 -7200
# Node ID 00b9a5073b01d4e2156cca66d67e78b7c2edd239
# Parent  9fbeb9b0aba0e22b4b68bb5a3ab879ddc7bbf87c
commented

diff -r 9fbeb9b0aba0 -r 00b9a5073b01 src/Pure/pure_thy.ML
--- 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]