# HG changeset patch
# User wenzelm
# Date 1191501731 -7200
# Node ID e1214fa781cae3be1a8dd0acec4fee05e69b798d
# Parent  137c242e72770b7d2a0d019131fd80b3a220ae53
avoid gensym;

diff -r 137c242e7277 -r e1214fa781ca src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Oct 04 13:26:34 2007 +0200
+++ b/src/Pure/Thy/present.ML	Thu Oct 04 14:42:11 2007 +0200
@@ -533,7 +533,9 @@
       let
         val base = Path.base path;
         val name =
-          (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
+          (case Path.implode (#1 (Path.split_ext base)) of
+            "" => "DUMMY" ^ serial_string ()
+          | s => s);
       in
         if File.exists path then
           (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)