src/HOL/Import/proof_kernel.ML
changeset 29281 b22ccb3998db
parent 29270 0eade173f77e
child 29289 f45c9c3b40a3
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 19:56:38 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 20:31:36 2008 +0100
     1.3 @@ -1149,8 +1149,8 @@
     1.4        val t = term_of ct
     1.5        val thy = theory_of_cterm ct
     1.6        val frees = OldTerm.term_frees t
     1.7 -      val freenames = OldTerm.add_term_free_names (t, [])
     1.8 -      fun is_old_name n = n mem_string freenames
     1.9 +      val freenames = Term.add_free_names t []
    1.10 +      val is_old_name = member (op =) freenames
    1.11        fun name_of (Free (n, _)) = n
    1.12          | name_of _ = ERR "name_of"
    1.13        fun new_name' bump map n =