# 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 =