# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 21d0b48a5fb5f19730ad26bec8d56f62b4eb900f
# Parent  693ddbbab9138d1dbe1eafbcc805da39ffa32bb9
less aggressive resolving

diff -r 693ddbbab913 -r 21d0b48a5fb5 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -1291,7 +1291,7 @@
                 (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
               |> K |> Goal.prove_sorry lthy [] [] goal
               |> Thm.close_derivation
-              |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}
               |> pair eqn_pos
               |> single