# HG changeset patch
# User wenzelm
# Date 880558453 -3600
# Node ID eb65491ae776d06b7ef4662806a05f5ed1d36033
# Parent  92707e24b62b62817428458e09f0943b4e470f81
removed merge_opts;

diff -r 92707e24b62b -r eb65491ae776 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 25 17:56:49 1997 +0100
+++ b/src/Pure/library.ML	Wed Nov 26 16:34:13 1997 +0100
@@ -68,11 +68,6 @@
 fun apsome f (Some x) = Some (f x)
   | apsome _ None = None;
 
-fun merge_opts _ (None, None) = None
-  | merge_opts _ (some as Some _, None) = some
-  | merge_opts _ (None, some as Some _) = some
-  | merge_opts merge (Some x, Some y) = Some (merge (x, y));
-
 (*handle partial functions*)
 fun can f x = (f x; true) handle _ => false;
 fun try f x = Some (f x) handle _ => None;
@@ -903,16 +898,15 @@
 
 fun newid n = 
   let 
-  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end
+  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
 
-  val seedr = ref 0;
+val seedr = ref 0;
 
 in
+
 fun init_gensym() = (seedr := 0);
 
-fun gensym pre = pre ^ 
-                 (#1(newid (!seedr), 
-                     seedr := 1+ !seedr))
+fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
 end;