--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 25 22:00:33 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 25 22:00:33 2012 +0200
@@ -1231,7 +1231,7 @@
| freeze t = t
in t |> exists_subterm is_Var t ? freeze end
-fun presimp_prop ctxt t =
+fun presimp_prop ctxt type_enc t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -1240,7 +1240,7 @@
val need_trueprop = (fastype_of t = @{typ bool})
in
t |> need_trueprop ? HOLogic.mk_Trueprop
- |> extensionalize_term ctxt
+ |> not (is_type_enc_higher_order type_enc) ? extensionalize_term ctxt
|> presimplify_term thy
|> HOLogic.dest_Trueprop
end
@@ -1796,7 +1796,7 @@
(0 upto length hyp_ts)
val ((conjs, facts), lam_facts) =
(conjs, facts)
- |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt))))
+ |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
|> (if lam_trans = no_lamsN then
rpair []
else