diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -1230,10 +1230,10 @@
       | _ => do_term bs t
   in do_formula [] end
 
-fun presimplify_term thy t =
+fun presimplify_term ctxt t =
   if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
-    t |> Skip_Proof.make_thm thy
-      |> Meson.presimplify
+    t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+      |> Meson.presimplify ctxt
       |> prop_of
   else
     t
@@ -1273,7 +1273,7 @@
     t |> need_trueprop ? HOLogic.mk_Trueprop
       |> (if is_ho then unextensionalize_def
           else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
-      |> presimplify_term thy
+      |> presimplify_term ctxt
       |> HOLogic.dest_Trueprop
   end
   handle TERM _ => @{const True}