src/HOL/Import/shuffler.ML
changeset 29281 b22ccb3998db
parent 29270 0eade173f77e
child 29287 5b0bfd63b5da
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 19:56:38 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 20:31:36 2008 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4                then
     1.5                    let
     1.6                        val cert = cterm_of thy
     1.7 -                      val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
     1.8 +                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
     1.9                        val cv = cert v
    1.10                        val ct = cert t
    1.11                        val th = (assume ct)
    1.12 @@ -384,7 +384,7 @@
    1.13                        Type("fun",[aT,bT]) =>
    1.14                        let
    1.15                            val cert = cterm_of thy
    1.16 -                          val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
    1.17 +                          val vname = Name.variant (Term.add_free_names t []) "v"
    1.18                            val v = Free(vname,aT)
    1.19                            val cv = cert v
    1.20                            val ct = cert t