| changeset 48539 | 0debf65972c7 |
| parent 48438 | 3e45c98fe127 |
| child 48799 | 5c9356f8c968 |
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Jul 27 08:52:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Jul 27 08:52:40 2012 +0200 @@ -216,7 +216,7 @@ dependencies in the TSTP proof. Remove the next line once this is fixed. *) add_non_rec_defs fact_names - else if rule = satallax_unsat_coreN then + else if rule = satallax_coreN then (fn [] => (* Satallax doesn't include definitions in its unsatisfiable cores, so we assume the worst and include them all here. *)