--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 06 15:58:56 2015 +0100
@@ -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.cterm_of thy predicate)]
+ |> Drule.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}