# HG changeset patch
# User paulson
# Date 961494633 -7200
# Node ID 96dcdd84f1e1e029b8529280f14fb1f521674e60
# Parent  453996655ac2fe7f0ba82dd2e40826fbb8f720dc
deleted a step made redundant by the improved rules for setsum

diff -r 453996655ac2 -r 96dcdd84f1e1 src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:42:24 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:50:33 2000 +0200
@@ -332,7 +332,6 @@
  by (Force_tac 1);
 by (Clarify_tac 1);
 by (ftac setsum_SucD 1);
- by (assume_tac 1);
 by (Clarify_tac 1);
 by (rename_tac "a" 1);
 by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);