diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri May 14 16:15:10 2010 +0200
@@ -20,9 +20,9 @@
      explicit_apply: bool,
      respect_no_atp: bool,
      relevance_threshold: real,
-     convergence: real,
+     relevance_convergence: real,
      theory_relevant: bool option,
-     follow_defs: bool,
+     defs_relevant: bool,
      isar_proof: bool,
      shrink_factor: int,
      timeout: Time.time,
@@ -79,9 +79,9 @@
    explicit_apply: bool,
    respect_no_atp: bool,
    relevance_threshold: real,
-   convergence: real,
+   relevance_convergence: real,
    theory_relevant: bool option,
-   follow_defs: bool,
+   defs_relevant: bool,
    isar_proof: bool,
    shrink_factor: int,
    timeout: Time.time,