--- 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