src/HOL/Tools/Function/scnp_reconstruct.ML

 
     fun get_desc_thm cidx m1 m2 bStrict =
       (case Termination.get_descent D (nth cs cidx) m1 m2 of
         SOME (Termination.Less thm) =>
           if bStrict then thm
-          else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
+          else (thm COMP (Thm.lift_rule (Thm.cprop_of thm) @{thm less_imp_le}))
       | SOME (Termination.LessEq (thm, _))  =>
           if not bStrict then thm
           else raise Fail "get_desc_thm"
       | _ => raise Fail "get_desc_thm")
 

       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)
-        |> cterm_of thy
+        |> Thm.cterm_of thy
     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)