1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -1199,11 +1199,13 @@
     1.4        | _ => do_term bs t
     1.5    in do_formula [] end
     1.6  
     1.7 -fun presimplify_term ctxt t =
     1.8 -  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
     1.9 -       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    1.10 -          #> Meson.presimplify
    1.11 -          #> prop_of)
    1.12 +fun presimplify_term thy t =
    1.13 +  if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
    1.14 +    t |> Skip_Proof.make_thm thy
    1.15 +      |> Meson.presimplify
    1.16 +      |> prop_of
    1.17 +  else
    1.18 +    t
    1.19  
    1.20  fun is_fun_equality (@{const_name HOL.eq},
    1.21                       Type (_, [Type (@{type_name fun}, _), _])) = true
    1.22 @@ -1252,7 +1254,7 @@
    1.23     in
    1.24       t |> need_trueprop ? HOLogic.mk_Trueprop
    1.25         |> extensionalize_term ctxt
    1.26 -       |> presimplify_term ctxt
    1.27 +       |> presimplify_term thy
    1.28         |> HOLogic.dest_Trueprop
    1.29     end
    1.30     handle TERM _ => default_formula role)