src/HOL/Tools/datatype_rep_proofs.ML

 (*  Title:      HOL/Tools/datatype_rep_proofs.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Definitional introduction of datatypes
 Proof of characteristic theorems:
 
  - injectivity of constructors
  - distinctness of constructors
  - induction theorem
-
 *)
 
 signature DATATYPE_REP_PROOFS =
 sig
   val distinctness_limit : int Config.T

     val leafTs' = get_nonrec_types descr' sorts;
     val branchTs = get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
       else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = get_arities descr' \ 0;
-    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
+    val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
     val oldTs = Library.drop (length (hd descr), recTs);
     val sumT = if null leafTs then HOLogic.unitT

     fun mk_funs_inv thy thm =
       let
         val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
-        val used = add_term_tfree_names (a, []);
+        val used = OldTerm.add_term_tfree_names (a, []);
 
         fun mk_thm i =
           let
             val Ts = map (TFree o rpair HOLogic.typeS)
               (Name.variant_list used (replicate i "'t"));