# HG changeset patch
# User lcp
# Date 804436764 -7200
# Node ID 39119c4c7bac1cae053d649ed0d19652e9a64d37
# Parent  5873833cf37f8f8b3fa02d5146f7cb2df01d19b8
Proof of n_leaves_reflect uses permutative rewriting.

diff -r 5873833cf37f -r 39119c4c7bac src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Thu Jun 29 16:33:17 1995 +0200
+++ b/src/ZF/ex/BT.ML	Thu Jun 29 16:39:24 1995 +0200
@@ -129,8 +129,7 @@
 val prems = goal BT.thy
     "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
 by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (asm_simp_tac bt_ss));
-by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute, n_leaves_type])));
 qed "n_leaves_reflect";
 
 val prems = goal BT.thy