# HG changeset patch
# User wenzelm
# Date 1316435480 -7200
# Node ID 6f27ecf2a9517245035416c813ff45e7524b38ea
# Parent  272e8e4e4fc7ff9ab04a5456d9f13de4ecfdf98a
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;

diff -r 272e8e4e4fc7 -r 6f27ecf2a951 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Sep 19 12:58:52 2011 +0200
+++ b/src/Pure/Thy/present.ML	Mon Sep 19 14:31:20 2011 +0200
@@ -499,8 +499,8 @@
         val base = Path.base path;
         val name =
           (case Path.implode (#1 (Path.split_ext base)) of
-            "" => "DUMMY" ^ serial_string ()
-          | s => s);
+            "" => "DUMMY"
+          | s => s)  ^ serial_string ();
       in
         if File.exists path then
           (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)