# HG changeset patch
# User clasohm
# Date 827492768 -3600
# Node ID 699ad6611c1e11f9158b3caa9817d41ca3a39e4c
# Parent  0ef6ea27ab15e3992dcd19cdc40a69221a065089
fixed incompatibility of add_to_parents with SML109's new Io exceptions

diff -r 0ef6ea27ab15 -r 699ad6611c1e src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Mar 21 13:02:26 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Mar 22 12:06:08 1996 +0100
@@ -671,9 +671,9 @@
 
                 val fname = tack_on path ("." ^ t ^ "_sub.html");
                 val out = if file_exists fname then
-                            open_append fname  handle Io s =>
-                              (warning ("Unable to write to file ." ^
-                                        fname); raise Io s)
+                            open_append fname  handle e  =>
+                              (warning ("Unable to write to file " ^
+                                        fname); raise e)
                           else raise MK_HTML;
             in output (out,
                  " |\n \\__<A HREF=\"" ^