--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Dec 13 21:56:15 2015 +0100
@@ -1579,8 +1579,7 @@
val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
lthy
|> Proof.theorem NONE after_qed goalss
- |> Proof.refine (Method.primitive_text (K I))
- |> Seq.hd) ooo primcorec_ursive_cmd false;
+ |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo