# HG changeset patch
# User paulson
# Date 932563050 -7200
# Node ID 8f246bc87ab2d78c4203ad904ef6932cb65de5a3
# Parent  4c201f27c74ea344c823c0f11f9463041526c233
tweaked proof after removal of diff_is_0_eq RS iffD2

diff -r 4c201f27c74e -r 8f246bc87ab2 src/HOL/UNITY/GenPrefix.ML
--- 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 |] \