diff -r a3793600cb93 -r 4d3527b94f2a src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -372,11 +372,10 @@
           |> snd
         end)
       [goals] |>
-    Proof.apply (Method.Basic (fn ctxt => fn _ =>
-      EMPTY_CASES
+    Proof.refine_singleton (Method.Basic (fn ctxt => fn _ =>
+      Method.CONTEXT_TACTIC
        (rewrite_goals_tac ctxt defs_thms THEN
-        compose_tac ctxt (false, rule, length rule_prems) 1))) |>
-    Seq.hd
+        compose_tac ctxt (false, rule, length rule_prems) 1)))
   end;
 
 in