# HG changeset patch
# User blanchet
# Date 1393847299 -3600
# Node ID e776a4b813d1ebceddb506316154ed5a723c495f
# Parent  48ced935c0e5e00741f21b79e2ac64b1399c2e18
use aconv to compare terms (for cleanliness)

diff -r 48ced935c0e5 -r e776a4b813d1 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:19 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:19 2014 +0100
@@ -97,7 +97,7 @@
 
 fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
   | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
-  | is_sum_prod_natLeq t = (t = @{term natLeq});
+  | is_sum_prod_natLeq t = t aconv @{term natLeq};
 
 fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
   let