# HG changeset patch
# User paulson
# Date 864306716 -7200
# Node ID cdcc4d5602b671cae95b7d1577eac5dd5b7de8a8
# Parent  4f5ffefa77992abf6d5f74d699e1cc44ac50d97e
Now the recdef induction rule variables are named u, v, ...

diff -r 4f5ffefa7799 -r cdcc4d5602b6 TFL/tfl.sml
--- 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;
 
 
 (*---------------------------------------------------------------------------
diff -r 4f5ffefa7799 -r cdcc4d5602b6 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Thu May 22 15:11:23 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Thu May 22 15:11:56 1997 +0200
@@ -88,7 +88,7 @@
 
 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
 goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
-by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1);
+by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq])));
@@ -112,7 +112,7 @@
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
 goal thy "!!k. (f dvd m) & (f dvd n) --> f dvd gcd(m,n)";
-by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1);
+by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [dvd_mod, mod_less_divisor,