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' (add_term_free_names (t, [])) [] t;
+fun strip_all t = strip_all' (OldTerm.add_term_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);
 

       | _ => vs)
     | (_, vs) => vs) [] (OldTerm.term_vars prop);
 
 fun dt_of_intrs thy vs nparms intrs =
   let
-    val iTs = term_tvars (prop_of (hd intrs));
+    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
     val Tvs = map TVar iTs;
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
     val params = map dest_Var (Library.take (nparms, ts));
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);

   | gen_rvar _ t = t;
 
 fun mk_realizes_eqn n vs nparms intrs =
   let
     val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
-    val iTs = term_tvars concl;
+    val iTs = OldTerm.term_tvars concl;
     val Tvs = map TVar iTs;
     val (h as Const (s, T), us) = strip_comb concl;
     val params = List.take (us, nparms);
     val elTs = List.drop (binder_types T, nparms);
     val predT = elTs ---> HOLogic.boolT;

       (Term.add_vars (prop_of intr) [] \\ params);
     val rule' = strip_all rule;
     val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
     val used = map (fst o dest_Free) args;
 
-    fun is_rec t = not (null (term_consts t inter rsets));
+    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
 
     fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
       | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
       | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
           Const (s, _) => can (InductivePackage.the_inductive ctxt) s

 
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let
     val qualifier = NameSpace.qualifier (name_of_thm induct);
     val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
-    val iTs = term_tvars (prop_of (hd intrs));
+    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
     val ar = length vs + length iTs;
     val params = InductivePackage.params_of raw_induct;
     val arities = InductivePackage.arities_of raw_induct;
     val nparms = length params;
     val params' = map dest_Var params;

             (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 add_term_free_names [] rlzs;
+        val used = foldr OldTerm.add_term_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