--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 11:03:02 2015 +0200
@@ -1449,7 +1449,7 @@
(the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
- |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
+ |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
@{thms eqTrueE eq_False[THEN iffD1] notnotD}
|> pair eqn_pos
|> single