# HG changeset patch
# User nipkow
# Date 847983696 -3600
# Node ID 6c217c071b977583d36b148f6a7f409286279248
# Parent  07c471510cf1f97ec01f6b827a01ae0a47da478d
Modified formal of thms in html file.

diff -r 07c471510cf1 -r 6c217c071b97 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Nov 14 14:38:51 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Thu Nov 14 16:01:36 1996 +0100
@@ -1095,7 +1095,7 @@
       in case !cur_htmlfile of
              Some out =>
                (mk_theorems_title out;
-                output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^
+                output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
                              escape 
 			      (explode 
 			       (string_of_thm (#1 (freeze_thaw thm)))) ^