src/HOL/Import/shuffler.ML
changeset 29270 0eade173f77e
parent 29269 5c25a2012975
child 29281 b22ccb3998db
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -247,8 +247,8 @@
     1.4  
     1.5  fun freeze_thaw_term t =
     1.6      let
     1.7 -        val tvars = term_tvars t
     1.8 -        val tfree_names = add_term_tfree_names(t,[])
     1.9 +        val tvars = OldTerm.term_tvars t
    1.10 +        val tfree_names = OldTerm.add_term_tfree_names(t,[])
    1.11          val (type_inst,_) =
    1.12              Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
    1.13                        let
    1.14 @@ -267,7 +267,7 @@
    1.15    | inst_tfrees thy ((name,U)::rest) thm =
    1.16      let
    1.17          val cU = ctyp_of thy U
    1.18 -        val tfrees = add_term_tfrees (prop_of thm,[])
    1.19 +        val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
    1.20          val (rens, thm') = Thm.varifyT'
    1.21      (remove (op = o apsnd fst) name tfrees) thm
    1.22          val mid =
    1.23 @@ -321,7 +321,7 @@
    1.24                then
    1.25                    let
    1.26                        val cert = cterm_of thy
    1.27 -                      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
    1.28 +                      val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
    1.29                        val cv = cert v
    1.30                        val ct = cert t
    1.31                        val th = (assume ct)
    1.32 @@ -384,7 +384,7 @@
    1.33                        Type("fun",[aT,bT]) =>
    1.34                        let
    1.35                            val cert = cterm_of thy
    1.36 -                          val vname = Name.variant (add_term_free_names(t,[])) "v"
    1.37 +                          val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
    1.38                            val v = Free(vname,aT)
    1.39                            val cv = cert v
    1.40                            val ct = cert t
    1.41 @@ -572,8 +572,8 @@
    1.42      fold_rev (fn thm => fn cs =>
    1.43                let
    1.44                    val (lhs,rhs) = Logic.dest_equals (prop_of thm)
    1.45 -                  val ignore_lhs = term_consts lhs \\ term_consts rhs
    1.46 -                  val ignore_rhs = term_consts rhs \\ term_consts lhs
    1.47 +                  val ignore_lhs = OldTerm.term_consts lhs \\ OldTerm.term_consts rhs
    1.48 +                  val ignore_rhs = OldTerm.term_consts rhs \\ OldTerm.term_consts lhs
    1.49                in
    1.50                    fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    1.51                end)