src/HOL/Tools/Transfer/transfer_bnf.ML

         val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else []
         val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1]
         val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
       in
         thm
-        |> Drule.instantiate' cTs cts
+        |> Thm.instantiate' cTs cts
         |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
           (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
         |> Local_Defs.unfold lthy eq_onps
         |> (fn thm => if conjuncts <> [] then @{thm box_equals}
               OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True]