src/ZF/ex/Ntree.ML

--- a/src/ZF/ex/Ntree.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Ntree.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -15,8 +15,7 @@
 
 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
 let open ntree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "ntree_unfold";
 
@@ -70,8 +69,7 @@
 
 goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
 let open maptree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "maptree_unfold";
 
@@ -95,8 +93,7 @@
 
 goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
 let open maptree2;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "maptree2_unfold";