src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41211 1e2e16bc0077
parent 41199 4698d12dd860
child 41313 a96ac4d180b7
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 15:44:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 15:46:54 2010 +0100
@@ -226,7 +226,7 @@
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
               |> transform_elim_term
-              |> atomize_term
+              |> Object_Logic.atomize_term thy
     val need_trueprop = (fastype_of t = HOLogic.boolT)
     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
               |> extensionalize_term