src/HOL/Nominal/nominal_primrec.ML

           |> Local_Theory.note
             ((qualify (Binding.name "simps"), @{attributes [simp, nitpick_simp]}), maps snd simps')
           |> 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
 
 val primrec = gen_primrec Specification.check_spec (K I);