changeset 54967 | 78de75e3e52a |
parent 54959 | 30ded82ff806 |
child 54968 | baa2baf29eff |
--- 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