src/HOL/Tools/Predicate_Compile/core_data.ML

     fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
       let
         fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
         fun inst_of_matches tts =
           fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
-          |> snd |> Vartab.dest |> map (apply2 (cterm_of thy) o term_pair_of)
+          |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of thy) o term_pair_of)
         val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
         val case_th =
           rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
         val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1
         val pats =

             (take nargs (Thm.prems_of case_th))
         val case_th' =
           Thm.instantiate ([], inst_of_matches pats) case_th
             OF replicate nargs @{thm refl}
         val thesis =
-          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems2)) case_th'
-            OF prems2
+          Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2))
+            case_th' OF prems2
       in rtac thesis 1 end
   in
     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule
       (fn {context = ctxt1, ...} =>
         eresolve_tac ctxt1 [pre_cases_rule] 1 THEN (fn st =>

         val thy = Proof_Context.theory_of ctxt
 
         val pos = Position.thread_data ()
         fun is_intro_of intro =
           let
-            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
+            val (const, _) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of intro))
           in (fst (dest_Const const) = name) end;
         val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
         val index = find_index (fn s => s = name) (#names (fst info))
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index

   in PredData.map cons_intro thy end
 
 fun set_elim thm =
   let
     val (name, _) =
-      dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
+      dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
   in
     PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
   end
 
 fun register_predicate (constname, intros, elim) thy =