# HG changeset patch
# User wenzelm
# Date 1001697787 -7200
# Node ID b325c05709d3f8257610bf2bd9634a8664ded5fd
# Parent  b95f527482fc56b73d244e47f8cc5ea52110433f
internal thm numbering with ":" instead of "_";

diff -r b95f527482fc -r b325c05709d3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Sep 28 19:22:40 2001 +0200
+++ b/src/Pure/pure_thy.ML	Fri Sep 28 19:23:07 2001 +0200
@@ -224,7 +224,7 @@
 (* naming *)
 
 fun gen_names len name =
-  map (fn i => name ^ "_" ^ string_of_int i) (1 upto len);
+  map (fn i => name ^ ":" ^ string_of_int i) (1 upto len);
 
 fun name_single name x = [(name, x)];
 fun name_multi name xs = gen_names (length xs) name ~~ xs;