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