src/HOL/Tools/record.ML
changeset 32758 cd47afaf0d78
parent 32757 4e97fc468a53
child 32760 ea6672bff5dd
     1.1 --- a/src/HOL/Tools/record.ML	Mon Sep 28 15:37:19 2009 +1000
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 14:25:42 2009 +1000
     1.3 @@ -86,11 +86,11 @@
     1.4  val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
     1.5  
     1.6  fun named_cterm_instantiate values thm = let
     1.7 -    fun match name (Var ((name', _), _)) = name = name'
     1.8 +    fun match name ((name', _), _) = name = name'
     1.9        | match name _ = false;
    1.10      fun getvar name = case (find_first (match name)
    1.11 -                                    (OldTerm.term_vars (prop_of thm)))
    1.12 -      of SOME var => cterm_of (theory_of_thm thm) var
    1.13 +                                    (Term.add_vars (prop_of thm) []))
    1.14 +      of SOME var => cterm_of (theory_of_thm thm) (Var var)
    1.15         | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    1.16    in
    1.17      cterm_instantiate (map (apfst getvar) values) thm