# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1254198342 -36000
# Node ID cd47afaf0d78d2b979a68ddca3de44ccace0779b
# Parent  4e97fc468a53a20d0c4360b694b13e9d22b2021b
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.

diff -r 4e97fc468a53 -r cd47afaf0d78 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Sep 28 15:37:19 2009 +1000
+++ b/src/HOL/Tools/record.ML	Tue Sep 29 14:25:42 2009 +1000
@@ -86,11 +86,11 @@
 val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
 
 fun named_cterm_instantiate values thm = let
-    fun match name (Var ((name', _), _)) = name = name'
+    fun match name ((name', _), _) = name = name'
       | match name _ = false;
     fun getvar name = case (find_first (match name)
-                                    (OldTerm.term_vars (prop_of thm)))
-      of SOME var => cterm_of (theory_of_thm thm) var
+                                    (Term.add_vars (prop_of thm) []))
+      of SOME var => cterm_of (theory_of_thm thm) (Var var)
        | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
   in
     cterm_instantiate (map (apfst getvar) values) thm