src/Provers/Arith/assoc_fold.ML

 
  val assoc_ss = Data.ss addsimps Data.add_ac;
 
  (*prove while suppressing timing information*)
  fun prove name ct tacf = 
-     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
+     setmp Library.timing false (prove_goalw_cterm [] ct) tacf
      handle ERROR =>
 	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
                 
  exception Assoc_fail;
 

 
 end;
 
 
 (*test data:
-set proof_timing;
+set timing;
 
 Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
 
 Goal "a + b + c + d + e + f + g + h + i + j + k + l + m + n + oo + p + q + r + s + t + u + v + (w + x + y + z + a + #2 + b + #2 + c + #2 + d + #2 + e) + #2 + f + (#2 + g + #2 + h + #2 + i) + #2 + (j + #2 + k + #2 + l + #2 + m + #2) + n + #2 + (oo + #2 + p + #2 + q + #2 + r) + #2 + s + #2 + t + #2 + u + #2 + v + #2 + w + #2 + x + #2 + y + #2 + z + #2 = (uu::nat)";
 *)