# HG changeset patch
# User blanchet
# Date 1284201050 -7200
# Node ID 5208954d906ce8cdf49dc0c1ce90efd7985d52b0
# Parent  05452dd66b2b471b4edbff617e40f96859f0ae0d
tuning

diff -r 05452dd66b2b -r 5208954d906c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 10:35:00 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 12:30:50 2010 +0200
@@ -122,10 +122,6 @@
   priority ("Available ATPs: " ^
             commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
 
-fun available_atps thy =
-  priority ("Available ATPs: " ^
-            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
 
 (* E prover *)