exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 12:30:05 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -886,8 +886,7 @@
   list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
 
 fun is_trivial_implies thm =
-  op aconv (Logic.dest_implies (Thm.prop_of thm))
-  handle TERM _ => false;
+  uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
 
 fun add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy =
   let