# HG changeset patch
# User wenzelm
# Date 958125164 -7200
# Node ID 7ec405405dd7063b3569f4650399321aeb18c3a0
# Parent  435187ffc64e288254f06e4483b3897c8abd7355
improved name of simproc;

diff -r 435187ffc64e -r 7ec405405dd7 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Wed May 10 22:34:30 2000 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Fri May 12 11:52:44 2000 +0200
@@ -68,7 +68,7 @@
    handle Assoc_fail => None;
  
  val conv = 
-     Simplifier.mk_simproc "assoc_fold_sums"
+     Simplifier.mk_simproc "assoc_fold"
        [Thm.cterm_of (Theory.sign_of Data.thy)
 	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
        proc;