# HG changeset patch
# User oheimb
# Date 835351020 -7200
# Node ID 245721624c8dbeb06eef0c577f158ed09c4b0697
# Parent  ffc20ff8019045b25b5b8a3fba1178ef25b05742
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)

diff -r ffc20ff80190 -r 245721624c8d src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Thu Jun 20 10:27:29 1996 +0200
+++ b/src/HOLCF/domain/library.ML	Fri Jun 21 11:57:00 1996 +0200
@@ -65,14 +65,15 @@
     fun nonreserved id = let val cs = explode id in
 			 if not(hd cs mem ["x","f","P"]) then id
 			 else implode(chr(1+ord (hd cs))::tl cs) end;
-    fun index_vnames(vn::vns,tab) =
-          (case assoc(tab,vn) of
+    fun index_vnames(vn::vns,occupied) =
+          (case assoc(occupied,vn) of
              None => if vn mem vns
-                     then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
-                     else  vn      :: index_vnames(vns,        tab)
-           | Some(i) => (vn^(string_of_int i)) :: index_vnames(vns,(vn,i+1)::tab))
-      | index_vnames([],tab) = [];
-in index_vnames(map (nonreserved o typid) types,[("o",1)]) end;
+                     then (vn^"1") :: index_vnames(vns,(vn,1)  ::occupied)
+                     else  vn      :: index_vnames(vns,          occupied)
+           | Some(i) => (vn^(string_of_int (i+1)))
+				   :: index_vnames(vns,(vn,i+1)::occupied))
+      | index_vnames([],occupied) = [];
+in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end;
 
 fun type_name_vars (Type(name,typevars)) = (name,typevars)
 |   type_name_vars _                     = Imposs "library:type_name_vars";