# HG changeset patch
# User clasohm
# Date 801749568 -7200
# Node ID 28e312a189461d3e7ee6b31a650739173bf9161c
# Parent  dfb29abcf3c26f67537f24b0c1d1e714814ccc51
replaced "All" by "all" in ThmdbFUN's ignore parameter

diff -r dfb29abcf3c2 -r 28e312a18946 src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Mon May 29 13:55:06 1995 +0200
+++ b/src/Pure/Thy/ROOT.ML	Mon May 29 14:12:48 1995 +0200
@@ -27,7 +27,7 @@
 fun init_thy_reader () =
   use_string
    ["structure ThmDB = \
-    \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);",
+    \ThmdbFUN(val ignore = [\"Trueprop\",\"all\",\"==>\",\"==\"]);",
     "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
                                    \and ThmDB = ThmDB);",
     "open Readthy ThmDB;"];