src/HOL/Tools/Function/function_elims.ML

         val (free_vars, prop, ranT, name_ctxt) = mk_funeq arity (fastype_of f) name_ctxt ([], f);
         val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
         val args = HOLogic.mk_tuple arg_vars;
         val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
+        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Thm.cterm_of ctxt
         val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
 
-        val cprop = Proof_Context.cterm_of ctxt prop;
+        val cprop = Thm.cterm_of ctxt prop;
 
-        val asms = [cprop, Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+        val asms = [cprop, Thm.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
         val asms_thms = map Thm.assume asms;
 
         fun prep_subgoal_tac i =
           REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
           THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i

           THEN bool_subst_tac ctxt i;
 
         val elim_stripped =
           nth cases idx
           |> Thm.forall_elim P
-          |> Thm.forall_elim (Proof_Context.cterm_of ctxt args)
+          |> Thm.forall_elim (Thm.cterm_of ctxt args)
           |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
           |> fold_rev Thm.implies_intr asms
-          |> Thm.forall_intr (Proof_Context.cterm_of ctxt rhs_var);
+          |> Thm.forall_intr (Thm.cterm_of ctxt rhs_var);
 
         val bool_elims =
           (case ranT of
             Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
           | _ => []);
 
         fun unstrip rl =
           rl
-          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) arg_vars
+          |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars
           |> Thm.forall_intr P
       in
         map unstrip (elim_stripped :: bool_elims)
       end;
   in