--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Jul 27 17:44:55 2015 +0200
@@ -153,7 +153,7 @@
val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
val predicate = lambda_tuple lhss (list_comb (P, lhss))
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
- |> Drule.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
+ |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
|> Local_Defs.unfold lthy @{thms split_conv}