changeset 41990 | 7f2793d51efc |
parent 41788 | adfd365c7ea4 |
child 42180 | a6c141925a8a |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 17 11:18:31 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 17 11:18:31 2011 +0100 @@ -246,7 +246,7 @@ else launch_provers state (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) - (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst)) + (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then