1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 17 11:18:31 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 17 11:18:31 2011 +0100
     1.3 @@ -246,7 +246,7 @@
     1.4          else
     1.5            launch_provers state
     1.6                (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
     1.7 -              (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
     1.8 +              (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
     1.9                (K (K NONE)) atps
    1.10        fun launch_smts accum =
    1.11          if null smts then