diff -r 785a59235a15 -r 1f4b011c5738 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Apr 19 12:06:34 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Apr 19 13:05:50 2016 +0200
@@ -375,9 +375,12 @@
   prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME));
 
 fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs =
-  (fn (goals, after_qed, _, lthy) =>
+  (fn (goals, after_qed, definitions, lthy) =>
     lthy
-    |> after_qed (map2 (single oo Goal.prove lthy [] []) goals (tacs (length goals)))) oo
+    |> after_qed (map2 (fn goal => fn tac => [Goal.prove lthy [] [] goal
+        (fn (ctxtprems as {context = ctxt, prems = _}) =>
+          unfold_thms_tac ctxt definitions THEN tac ctxtprems)])
+      goals (tacs (length goals)))) oo
   prepare_common prepare_name prepare_typ prepare_sort prepare_thm;
 
 in