src/HOL/Tools/inductive_realizer.ML

       in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
       t $ strip_all' used names Q
   | strip_all' _ _ t = t;
 
-fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
+fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
 
 fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
       (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
   | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
 

             (hd (prems_of (hd inducts))))), nparms))) vs;
         val rs = indrule_realizer thy induct raw_induct rsets params'
           (vs' @ Ps) rec_names rss' intrs dummies;
         val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
           (prop_of ind)) (rs ~~ inducts);
-        val used = foldr OldTerm.add_term_free_names [] rlzs;
+        val used = fold Term.add_free_names rlzs [];
         val rnames = Name.variant_list used (replicate (length inducts) "r");
         val rnames' = Name.variant_list
           (used @ rnames) (replicate (length intrs) "s");
         val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
           let