src/HOL/Tools/BNF/bnf_gfp.ML

                   HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
               phis jsets Jzs Jzs';
           in
             @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
               ((set_minimal
-                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
+                |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
                 |> unfold_thms lthy incls) OF
                 (replicate n ballI @
                   maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
               |> singleton (Proof_Context.export names_lthy lthy)
               |> rule_by_tactic lthy (ALLGOALS (TRY o etac lthy asm_rl)))

               |> Thm.cterm_of lthy;
 
             val cphis = @{map 9} mk_cphi
               Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
 
-            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
+            val coinduct = Thm.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));