removed merge_opts;
authorwenzelm
Wed Nov 26 16:34:13 1997 +0100 (1997-11-26)
changeset 4284eb65491ae776
parent 4283 92707e24b62b
child 4285 05af145a61d4
removed merge_opts;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Nov 25 17:56:49 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 26 16:34:13 1997 +0100
     1.3 @@ -68,11 +68,6 @@
     1.4  fun apsome f (Some x) = Some (f x)
     1.5    | apsome _ None = None;
     1.6  
     1.7 -fun merge_opts _ (None, None) = None
     1.8 -  | merge_opts _ (some as Some _, None) = some
     1.9 -  | merge_opts _ (None, some as Some _) = some
    1.10 -  | merge_opts merge (Some x, Some y) = Some (merge (x, y));
    1.11 -
    1.12  (*handle partial functions*)
    1.13  fun can f x = (f x; true) handle _ => false;
    1.14  fun try f x = Some (f x) handle _ => None;
    1.15 @@ -903,16 +898,15 @@
    1.16  
    1.17  fun newid n = 
    1.18    let 
    1.19 -  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end
    1.20 +  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
    1.21  
    1.22 -  val seedr = ref 0;
    1.23 +val seedr = ref 0;
    1.24  
    1.25  in
    1.26 +
    1.27  fun init_gensym() = (seedr := 0);
    1.28  
    1.29 -fun gensym pre = pre ^ 
    1.30 -                 (#1(newid (!seedr), 
    1.31 -                     seedr := 1+ !seedr))
    1.32 +fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
    1.33  end;
    1.34  
    1.35