# HG changeset patch
# User paulson
# Date 962273708 -7200
# Node ID 68ecc04785f130ecedf0d2438eabcf5a83efea33
# Parent  7b2f4e6538b42d280691d63418c11d3129c2285a
fixed proof to cope with the default of equalityCE instead of equalityE

diff -r 7b2f4e6538b4 -r 68ecc04785f1 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Jun 29 12:14:45 2000 +0200
+++ b/src/HOL/List.ML	Thu Jun 29 12:15:08 2000 +0200
@@ -477,6 +477,8 @@
 
 Goal "set[i..j(] = {k. i <= k & k < j}";
 by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac ssubst 1);
 by Auto_tac;
 by (arith_tac 1);
 qed "set_upt";