TFL/tfl.sml
changeset 3301 cdcc4d5602b6
parent 3245 241838c01caf
child 3333 0bbf06e86c06
--- a/TFL/tfl.sml	Thu May 22 15:11:23 1997 +0200
+++ b/TFL/tfl.sml	Thu May 22 15:11:56 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/tfl
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Main TFL functor
+*)
+
 functor TFL(structure Rules : Rules_sig
             structure Thry  : Thry_sig
             structure Thms  : Thms_sig
@@ -54,25 +62,21 @@
  * The next function is common to pattern-match translation and 
  * proof of completeness of cases for the induction theorem.
  *
- * "gvvariant" make variables that are guaranteed not to be in vlist and
- * furthermore, are guaranteed not to be equal to each other. The names of
- * the variables will start with "v" and end in a number.
+ * The curried function "gvvariant" returns a function to generate distinct
+ * variables that are guaranteed not to be in vlist.  The names of
+ * the variables go u, v, ..., z, aa, ..., az, ...  The returned 
+ * function contains embedded refs!
  *---------------------------------------------------------------------------*)
-local val counter = ref 0
-in
 fun gvvariant vlist =
   let val slist = ref (map (#Name o S.dest_var) vlist)
-      val mem = U.mem (curry (op=))
-      val dummy = counter := 0
-      fun pass str = 
-         if (mem str (!slist)) 
-         then ( counter := !counter + 1;
-                pass (U.concat"v" (Int.toString(!counter))))
-         else (slist := str :: !slist; str)
+      val vname = ref "u"
+      fun new() = 
+         if !vname mem_string (!slist)
+         then (vname := bump_string (!vname);  new())
+         else (slist := !vname :: !slist;  !vname)
   in 
-  fn ty => S.mk_var{Name=pass "v",  Ty=ty}
-  end
-end;
+  fn ty => Free(new(), ty)
+  end;
 
 
 (*---------------------------------------------------------------------------