src/HOL/Tools/Function/scnp_reconstruct.ML

       Abs ("x", Termination.get_types D p, mk_set nat_pairT (map (tag_pair p) lm))
 
     val level_mapping =
       map_index pt_lev lev
         |> Termination.mk_sumcases D (setT nat_pairT)
-        |> Proof_Context.cterm_of ctxt
+        |> Thm.cterm_of ctxt
     in
       PROFILE "Proof Reconstruction"
         (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
          THEN (rtac @{thm reduction_pair_lemma} 1)
          THEN (rtac @{thm rp_inv_image_rp} 1)