src/HOL/Tools/coinduction.ML

         if P x then (x :: ins, outs) else (ins, x :: outs)
       end;
 
 fun ALLGOALS_SKIP skip tac st =
   let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
-  in doall (nprems_of st) st  end;
+  in doall (Thm.nprems_of st) st  end;
 
 fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
   st |> (tac1 i THEN (fn st' =>
-    Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
+    Seq.INTERVAL tac2 (i + skip) (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
 
 fun DELETE_PREMS_AFTER skip tac i st =
   let
-    val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
+    val n = nth (Thm.prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
   in
     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
   end;
 
 fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>

       Object_Logic.rulify_tac ctxt THEN'
       Method.insert_tac prems THEN'
       Object_Logic.atomize_prems_tac ctxt THEN'
       DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
         let
-          val vars = raw_vars @ map (term_of o snd) params;
+          val vars = raw_vars @ map (Thm.term_of o snd) params;
           val names_ctxt = ctxt
             |> fold Variable.declare_names vars
             |> fold Variable.declare_thm (raw_thm :: prems);
           val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
           val (rhoTs, rhots) = Thm.match (thm_concl, concl)
-            |>> map (apply2 typ_of)
-            ||> map (apply2 term_of);
+            |>> map (apply2 Thm.typ_of)
+            ||> map (apply2 Thm.term_of);
           val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
             |> map (subst_atomic_types rhoTs);
           val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
           val eqs =
             @{map 3} (fn name => fn T => fn (_, rhs) =>
               HOLogic.mk_eq (Free (name, T), rhs))
             names Ts raw_eqs;
-          val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
+          val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
             |> try (Library.foldr1 HOLogic.mk_conj)
             |> the_default @{term True}
             |> Ctr_Sugar_Util.list_exists_free vars
             |> Term.map_abs_vars (Variable.revert_fixed ctxt)
             |> fold_rev Term.absfree (names ~~ Ts)

                      let
                        val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
                        val inv_thms = init @ [last];
                        val eqs = take e inv_thms;
                        fun is_local_var t =
-                         member (fn (t, (_, t')) => t aconv (term_of t')) params t;
-                        val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
+                         member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
+                        val (eqs, assms') =
+                          filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
                         val assms = assms' @ drop e inv_thms
                       in
                         HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
                         Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
                       end)) ctxt)))])
         end) ctxt) THEN'
       K (prune_params_tac ctxt))
     #> Seq.maps (fn st =>
-      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
+      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
   end));
 
 local
 
 val ruleN = "rule"