# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID eaf0ffea11aaa6ad5f99d6e7ddaa0059d23e294f
# Parent  6df6e56fd7cd5f50bc3a1d2a8ff357f46bb5a015
tuning

diff -r 6df6e56fd7cd -r eaf0ffea11aa src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -1199,11 +1199,13 @@
       | _ => do_term bs t
   in do_formula [] end
 
-fun presimplify_term ctxt t =
-  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
-       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-          #> Meson.presimplify
-          #> prop_of)
+fun presimplify_term thy t =
+  if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
+    t |> Skip_Proof.make_thm thy
+      |> Meson.presimplify
+      |> prop_of
+  else
+    t
 
 fun is_fun_equality (@{const_name HOL.eq},
                      Type (_, [Type (@{type_name fun}, _), _])) = true
@@ -1252,7 +1254,7 @@
    in
      t |> need_trueprop ? HOLogic.mk_Trueprop
        |> extensionalize_term ctxt
-       |> presimplify_term ctxt
+       |> presimplify_term thy
        |> HOLogic.dest_Trueprop
    end
    handle TERM _ => default_formula role)