tweaked proof after removal of diff_is_0_eq RS iffD2

--- a/src/HOL/UNITY/GenPrefix.ML	Wed Jul 21 15:16:32 1999 +0200
+++ b/src/HOL/UNITY/GenPrefix.ML	Wed Jul 21 15:17:30 1999 +0200
@@ -137,7 +137,7 @@
 \     ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r";
 by (etac genPrefix.induct 1);
 by (forward_tac [genPrefix_length_le] 3);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2])));
 qed "genPrefix_take_append";
 
 Goal "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |] \