src/HOLCF/domain/library.ML
changeset 3428 34655a5d2f56
parent 3176 a3db6c177885
child 4008 2444085532c6
--- a/src/HOLCF/domain/library.ML	Fri Jun 06 13:28:40 1997 +0200
+++ b/src/HOLCF/domain/library.ML	Fri Jun 06 16:02:13 1997 +0200
@@ -63,9 +63,7 @@
     fun typid (Type  (id,_)   ) = hd     (explode id)
       | typid (TFree (id,_)   ) = hd (tl (explode id))
       | typid (TVar ((id,_),_)) = hd (tl (explode id));
-    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 nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
     fun index_vnames(vn::vns,occupied) =
           (case assoc(occupied,vn) of
              None => if vn mem vns