src/Pure/Thy/present.ML
changeset 24829 e1214fa781ca
parent 24561 7b4aa14d2491
child 26323 73efc70edeef
     1.1 --- a/src/Pure/Thy/present.ML	Thu Oct 04 13:26:34 2007 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Oct 04 14:42:11 2007 +0200
     1.3 @@ -533,7 +533,9 @@
     1.4        let
     1.5          val base = Path.base path;
     1.6          val name =
     1.7 -          (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
     1.8 +          (case Path.implode (#1 (Path.split_ext base)) of
     1.9 +            "" => "DUMMY" ^ serial_string ()
    1.10 +          | s => s);
    1.11        in
    1.12          if File.exists path then
    1.13            (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)