# HG changeset patch
# User wenzelm
# Date 1007409697 -3600
# Node ID e7b1956f4eae95df8da62a1d71b3bd737a035f2c
# Parent  5d1436d1c268bcb9715ee92dbbe60607a8464b2c
removed questionable init_gensym;

diff -r 5d1436d1c268 -r e7b1956f4eae src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Dec 03 21:01:11 2001 +0100
+++ b/src/Provers/blast.ML	Mon Dec 03 21:01:37 2001 +0100
@@ -1186,9 +1186,7 @@
 		       lim   = lim}  :: brs)
 	  end
        | prv (tacs, trs, choices, _ :: brs) = backtrack choices
- in init_gensym();
-    prv ([], [], [(!ntrail, length brs, PROVE)], brs) 
- end;
+ in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
 
 
 (*Construct an initial branch.*)
diff -r 5d1436d1c268 -r e7b1956f4eae src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Dec 03 21:01:11 2001 +0100
+++ b/src/Pure/library.ML	Mon Dec 03 21:01:37 2001 +0100
@@ -278,7 +278,6 @@
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val transitive_closure: (string * string list) list -> (string * string list) list
-  val init_gensym: unit -> unit    (* FIXME !!??! *)
   val gensym: string -> string
   val bump_int_list: string list -> string list
   val bump_list: string list * string -> string list
@@ -1349,9 +1348,8 @@
 
 in
 
-fun init_gensym() = (seedr := 0);    (* FIXME !!??! *)
+fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
 
-fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
 end;