diff -r dc281bd5ca0a -r a3f592e3f4bd src/ZF/UNITY/Merge.ML
--- a/src/ZF/UNITY/Merge.ML	Fri May 30 11:44:29 2003 +0200
+++ b/src/ZF/UNITY/Merge.ML	Mon Jun 02 11:17:52 2003 +0200
@@ -111,7 +111,7 @@
 by (blast_tac (claset() addDs [ltD]) 1); 
 by (Clarify_tac 1); 
 by (subgoal_tac "length(x ` iOut) : nat" 1);
-by Typecheck_tac; 
+by (Asm_full_simp_tac 2);
 by (subgoal_tac "xa : nat" 1); 
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
 by (blast_tac (claset() addIs [lt_trans]) 2);