--- 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);