diff -r 28eb608b9b59 -r 0478ba10152a src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 25 23:01:31 2015 +0200
@@ -552,9 +552,10 @@
           |> map_filter (try (fn (x, [y]) =>
             (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map (fn (user_eqn, num_extra_args, rec_thm) =>
-              mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
-                def_thms rec_thm
-              |> K |> Goal.prove_sorry lthy' [] [] user_eqn
+              Goal.prove_sorry lthy' [] [] user_eqn
+                (fn {context = ctxt, prems = _} =>
+                  mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
+                    def_thms rec_thm)
               |> Thm.close_derivation);
       in
         ((js, simps), lthy')