src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

             if n = 1 then @{const True}
             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
         val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
 
-        fun mk_case_split' cp = Drule.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
+        fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
 
         val case_splitss' = map (map mk_case_split') cpss;
 
         val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
 

 
     fun mk_corec_sel_thm corec_thm sel sel_thm =
       let
         val (domT, ranT) = dest_funT (fastype_of sel);
         val arg_cong' =
-          Drule.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
+          Thm.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
             [NONE, NONE, SOME (Thm.cterm_of lthy sel)] arg_cong
           |> Thm.varifyT_global;
         val sel_thm' = sel_thm RSN (2, trans);
       in
         corec_thm RS arg_cong' RS sel_thm'