src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -376,7 +376,7 @@
     Proof.apply (Method.Basic (fn ctxt => fn _ =>
       NO_CASES
        (rewrite_goals_tac ctxt defs_thms THEN
-        compose_tac (false, rule, length rule_prems) 1))) |>
+        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
     Seq.hd
   end;