# HG changeset patch
# User wenzelm
# Date 809020992 -7200
# Node ID b4056a71eca2983ca7e7d4e55b7048728ba845fa
# Parent  56ee5cc3551004d7bee73cac4324e8db5942a0fb
minor fix to make less noise with SML/NJ;

diff -r 56ee5cc35510 -r b4056a71eca2 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Aug 18 16:38:41 1995 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Mon Aug 21 18:03:12 1995 +0200
@@ -415,7 +415,7 @@
         \\n\
         \|> add_thyname " ^ quote thy_name ^ ";\n\
         \\n\
-        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
+        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
         \\n\
         \\n"
         ^ postxt ^ "\n\
@@ -430,7 +430,7 @@
         \\n\
         \val thy = thy\n\
         \\n\
-        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
+        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
         \\n\
         \end;\n");