--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Mar 06 23:56:43 2015 +0100
@@ -469,7 +469,7 @@
val T = mk_tupleT_balanced tfrees;
in
@{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of @{theory} T)] []
+ |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
|> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
|> Thm.varifyT_global