src/HOL/Tools/BNF/bnf_def.ML
changeset 67222 19809bc9d7ff
parent 66272 c6714a9562ae
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Sat Dec 16 22:32:04 2017 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Dec 17 08:42:59 2017 +0100
     1.3 @@ -1904,7 +1904,8 @@
     1.4              Goal.prove_sorry lthy vars [] goal
     1.5                (fn {context = ctxt, prems = _} =>
     1.6                  HEADGOAL (rtac ctxt (pred_set RSN (2, pred_set RSN (2, box_equals)))) THEN
     1.7 -                unfold_thms_tac ctxt (@{thm Ball_image_comp} :: map Lazy.force set_map) THEN
     1.8 +                unfold_thms_tac ctxt
     1.9 +                  (@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN
    1.10                  HEADGOAL (rtac ctxt refl))
    1.11              |> Thm.close_derivation
    1.12            end;