1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 15:28:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:04:09 2010 +0200
     1.3 @@ -493,7 +493,7 @@
     1.4        repair_conjecture_shape_and_theorem_names output conjecture_shape
     1.5                                                  internal_thm_names
     1.6  
     1.7 -    val (message, relevant_thm_names) =
     1.8 +    val (message, used_thm_names) =
     1.9        case outcome of
    1.10          NONE =>
    1.11          proof_text isar_proof
    1.12 @@ -503,7 +503,7 @@
    1.13        | SOME failure => (string_for_failure failure ^ "\n", [])
    1.14    in
    1.15      {outcome = outcome, message = message, pool = pool,
    1.16 -     relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = msecs,
    1.17 +     used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
    1.18       output = output, proof = proof, internal_thm_names = internal_thm_names,
    1.19       conjecture_shape = conjecture_shape,
    1.20       filtered_clauses = the_filtered_clauses}