src/Provers/Arith/assoc_fold.ML

   val is_numeral: term -> bool
 end;
 
 signature ASSOC_FOLD =
 sig
-  val proc: simpset -> term -> thm option
+  val proc: Proof.context -> term -> thm option
 end;
 
 functor Assoc_Fold(Data: ASSOC_FOLD_DATA): ASSOC_FOLD =
 struct
 

       then sift_terms plus (x, sift_terms plus (y, (lits,others)))
       else (lits, t::others)    (*arbitrary summand*)
   | _ => (lits, t::others));
 
 (*A simproc to combine all literals in a associative nest*)
-fun proc ss lhs =
+fun proc ctxt lhs =
   let
     val plus = (case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern")
     val (lits, others) = sift_terms plus (lhs, ([],[]))
     val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*)
     val rhs = plus $ mk_sum plus lits $ mk_sum plus others
-    val th = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (lhs, rhs))
-      (fn _ => rtac Data.eq_reflection 1 THEN
-          simp_tac (Simplifier.inherit_context ss Data.assoc_ss) 1)
+    val th = Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs))
+      (fn _ => rtac Data.eq_reflection 1 THEN simp_tac (put_simpset Data.assoc_ss ctxt) 1)
   in SOME th end handle Assoc_fail => NONE;
 
 end;