# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1254116239 -36000
# Node ID 4e97fc468a53a20d0c4360b694b13e9d22b2021b
# Parent  fb32a99a7689cada260d5b0272c6bedc64f91aa7
Avoid a possible variable name conflict in instantiating a theorem.

Instantiating a theorem variable with new variables created a possible
variable name conflict if a record was defined with a field named
'f', 'x' etc. Using variable indices of 1 avoids the problem.

diff -r fb32a99a7689 -r 4e97fc468a53 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Sep 28 14:16:01 2009 +1000
+++ b/src/HOL/Tools/record.ML	Mon Sep 28 15:37:19 2009 +1000
@@ -2005,9 +2005,6 @@
 
     val r_rec0 = mk_rec all_vars_more 0;
     val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
-    val r_rec0_Vars = let
-        fun to_Var (Free (c, T)) = Var ((c, 0), T);
-      in mk_rec (map to_Var all_vars_more) 0 end;
 
     fun r n = Free (rN, rec_schemeT n)
     val r0 = r 0;
@@ -2075,6 +2072,12 @@
        pair, from which we can derive the bodies of our selector and
        updator and their convs. *)
     fun get_access_update_thms () = let
+        val r_rec0_Vars = let
+            (* pick variable indices of 1 to avoid possible variable
+               collisions with existing variables in updacc_eq_triv *)
+            fun to_Var (Free (c, T)) = Var ((c, 1), T);
+          in mk_rec (map to_Var all_vars_more) 0 end;
+
         val cterm_rec = cterm_of extension_thy r_rec0;
         val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
         val insts     = [("v", cterm_rec), ("v'", cterm_vrs)];