src/HOL/Tools/TFL/tfl.ML

 (*  Title:      HOL/Tools/TFL/tfl.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
 First part of main module.
 *)
 
 signature PRIM =

      val atom = single (distinct (op aconv) funcs)
      val (fname,ftype) = dest_atom atom
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
                               map (fn (t,i) => (t,(i,true))) (enumerate R))
-     val names = foldr add_term_names [] R
+     val names = foldr OldTerm.add_term_names [] R
      val atype = type_of(hd pats)
      and aname = Name.variant names "a"
      val a = Free(aname,atype)
      val ty_info = Thry.match_info thy
      val ty_match = Thry.match_type thy

                  else ()
      val (case_rewrites,context_congs) = extraction_thms thy
      val tych = Thry.typecheck thy
      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
      val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
-     val R = Free (Name.variant (foldr add_term_names [] eqns) Rname,
+     val R = Free (Name.variant (foldr OldTerm.add_term_names [] eqns) Rname,
                    Rtype)
      val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
      val dummy =
            if !trace then

 
 fun complete_cases thy =
  let val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
- let val names = foldr add_term_names [] pats
+ let val names = foldr OldTerm.add_term_names [] pats
      val T = type_of (hd pats)
      val aname = Name.variant names "a"
      val vname = Name.variant (aname::names) "v"
      val a = Free (aname, T)
      val v = Free (vname, T)

 let val tych = Thry.typecheck thy
     val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
-    val Pname = Name.variant (foldr (Library.foldr add_term_names)
+    val Pname = Name.variant (foldr (Library.foldr OldTerm.add_term_names)
                               [] (pats::TCsl)) "P"
     val P = Free(Pname, domain --> HOLogic.boolT)
     val Sinduct = R.SPEC (tych P) Sinduction
     val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case fconst thy) tasks
-    val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases))
+    val v = Free (Name.variant (foldr OldTerm.add_term_names [] (map concl proved_cases))
                     "v",
                   domain)
     val vtyped = tych v
     val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
     val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')