--- a/src/HOL/Tools/Function/function_core.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Tue Feb 10 14:48:26 2015 +0100
@@ -707,8 +707,8 @@
|> cterm_of thy
in
Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (auto_tac ctxt)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)