diff -r f93f7d766895 -r 56610e2ba220 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Tue Aug 06 11:20:47 2002 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Tue Aug 06 11:22:05 2002 +0200
@@ -11,12 +11,12 @@
 
 signature ASSOC_FOLD_DATA =
 sig
-  val ss		: simpset	(*basic simpset of object-logtic*)
-  val eq_reflection	: thm		(*object-equality to meta-equality*)
-  val sg_ref 		: Sign.sg_ref	(*the operator's signature*)
-  val T			: typ		(*the operator's numeric type*)
-  val plus		: term		(*the operator being folded*)
-  val add_ac		: thm list      (*AC-rewrites for plus*)
+  val ss                : simpset       (*basic simpset of object-logtic*)
+  val eq_reflection     : thm           (*object-equality to meta-equality*)
+  val sg_ref            : Sign.sg_ref   (*the operator's signature*)
+  val T                 : typ           (*the operator's numeric type*)
+  val plus              : term          (*the operator being folded*)
+  val add_ac            : thm list      (*AC-rewrites for plus*)
 end;
 
 
@@ -26,11 +26,11 @@
  val assoc_ss = Data.ss addsimps Data.add_ac;
 
  (*prove while suppressing timing information*)
- fun prove name ct tacf = 
+ fun prove name ct tacf =
      setmp Library.timing false (prove_goalw_cterm [] ct) tacf
      handle ERROR =>
-	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
-                
+         error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
+
  exception Assoc_fail;
 
  fun mk_sum []  = raise Assoc_fail
@@ -39,13 +39,13 @@
  (*Separate the literals from the other terms being combined*)
  fun sift_terms (t, (lits,others)) =
      case t of
-	  Const("Numeral.number_of", _) $ _ =>
-	      (t::lits, others)         (*new literal*)
-	| (f as Const _) $ x $ y =>
-	      if f = Data.plus 
+          Const("Numeral.number_of", _) $ _ =>
+              (t::lits, others)         (*new literal*)
+        | (f as Const _) $ x $ y =>
+              if f = Data.plus
               then sift_terms (x, sift_terms (y, (lits,others)))
-	      else (lits, t::others)    (*arbitrary summand*)
-	| _ => (lits, t::others);
+              else (lits, t::others)    (*arbitrary summand*)
+        | _ => (lits, t::others);
 
  val trace = ref false;
 
@@ -53,25 +53,23 @@
  fun proc sg _ lhs =
    let fun show t = string_of_cterm (Thm.cterm_of sg t)
        val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
-	       else ()
+               else ()
        val (lits,others) = sift_terms (lhs, ([],[]))
        val _ = if length lits < 2
                then raise Assoc_fail (*we can't reduce the number of terms*)
-               else ()  
+               else ()
        val rhs = Data.plus $ mk_sum lits $ mk_sum others
        val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
-       val th = prove "assoc_fold" 
-	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
-		   (fn _ => [rtac Data.eq_reflection 1,
-			     simp_tac assoc_ss 1])
+       val th = prove "assoc_fold"
+                   (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
+                   (fn _ => [rtac Data.eq_reflection 1,
+                             simp_tac assoc_ss 1])
    in Some th end
    handle Assoc_fail => None;
- 
- val conv = 
-     Simplifier.mk_simproc "assoc_fold"
-       [Thm.cterm_of (Sign.deref Data.sg_ref)
-	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
-       proc;
+
+ val conv =
+     Simplifier.simproc_i (Sign.deref Data.sg_ref) "assoc_fold"
+       [Data.plus $ Free ("x", Data.T) $ Free ("y",Data.T)] proc;
 
 end;