# HG changeset patch
# User paulson
# Date 961494681 -7200
# Node ID 7141b912b0bb35a788b1f3c1da57c154f7394e50
# Parent  96dcdd84f1e1e029b8529280f14fb1f521674e60
changed a step for the improved rules for setsum

diff -r 96dcdd84f1e1 -r 7141b912b0bb src/HOL/UNITY/AllocBase.ML
--- a/src/HOL/UNITY/AllocBase.ML	Tue Jun 20 11:50:33 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML	Tue Jun 20 11:51:21 2000 +0200
@@ -106,19 +106,17 @@
 by Auto_tac;
 qed "bag_of_sublist_lemma";
 
-
 Goal "finite A \
 \     ==> bag_of (sublist l A) = \
 \         setsum (%i. if i < length l then {# nth l i #} else {#}) A";
 by (res_inst_tac [("xs","l")] rev_induct 1);
 by (Simp_tac 1);
 by (stac (symmetric Zero_def) 1);
-by (etac (setsum_0 RS sym) 1);
+by (rtac (setsum_0 RS sym) 1);
 by (asm_simp_tac (simpset() addsimps [sublist_append, 
 				      bag_of_sublist_lemma]) 1);
 qed "bag_of_sublist";
 
-
 Goal "[| finite A; finite B |] \
 \     ==> bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
 \         bag_of (sublist l A) + bag_of (sublist l B)";