# HG changeset patch # User blanchet # Date 1473593725 -7200 # Node ID 4f8c6e63bc41aa92892760a77b849917e3f8fa4e # Parent 6a757f36997e245b84119d0076fdfd9d5ebae1a6 tuning diff -r 6a757f36997e -r 4f8c6e63bc41 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 00:14:44 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:25 2016 +0200 @@ -77,13 +77,13 @@ val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; val basic_sumprod_thms_set = @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib - o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; + o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; fun is_def_looping def = (case Thm.prop_of def of - Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op =) lhs) rhs + Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op aconv) lhs) rhs | _ => false); fun hhf_concl_conv cv ctxt ct =