diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -1838,7 +1838,7 @@
 
         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;
 
@@ -1864,7 +1864,7 @@
       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);