src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -373,8 +373,8 @@
           |> snd
         end)
       [goals] |>
-    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
-      rewrite_goals_tac defs_thms THEN
+    Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
+      rewrite_goals_tac ctxt defs_thms THEN
       compose_tac (false, rule, length rule_prems) 1))) |>
     Seq.hd
   end;