src/HOL/Tools/Function/fun_cases.ML

       Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
         handle TERM _ => err ();
     val info = Function.get_info ctxt f handle List.Empty => err ();
     val {elims, pelims, is_partial, ...} = info;
     val elims = if is_partial then pelims else the elims;
-    val cprop = Proof_Context.cterm_of ctxt prop;
+    val cprop = Thm.cterm_of ctxt prop;
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
       |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in