minor fix to make less noise with SML/NJ;
authorwenzelm
Mon Aug 21 18:03:12 1995 +0200 (1995-08-21)
changeset 1235b4056a71eca2
parent 1234 56ee5cc35510
child 1236 b54d51df9065
minor fix to make less noise with SML/NJ;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Aug 18 16:38:41 1995 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Aug 21 18:03:12 1995 +0200
     1.3 @@ -415,7 +415,7 @@
     1.4          \\n\
     1.5          \|> add_thyname " ^ quote thy_name ^ ";\n\
     1.6          \\n\
     1.7 -        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
     1.8 +        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
     1.9          \\n\
    1.10          \\n"
    1.11          ^ postxt ^ "\n\
    1.12 @@ -430,7 +430,7 @@
    1.13          \\n\
    1.14          \val thy = thy\n\
    1.15          \\n\
    1.16 -        \val () = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.17 +        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.18          \\n\
    1.19          \end;\n");
    1.20