src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

 val unfold_lets = @{thms Let_def[abs_def] split_beta}
 
 fun exhaust_inst_as_projs ctxt frees thm =
   let
     val num_frees = length frees;
-    val fs = Term.add_vars (prop_of thm) [] |> filter (can dest_funT o snd);
+    val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
     fun find s = find_index (curry (op =) s) frees;
     fun mk_cfp (f as ((s, _), T)) =
       (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T num_frees (find s)));
     val cfps = map mk_cfp fs;
   in

   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
     (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
 
 fun inst_split_eq ctxt split =
-  (case prop_of split of
+  (case Thm.prop_of split of
     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
       val split' = Drule.instantiate' [] [SOME (Proof_Context.cterm_of ctxt eq)] split;