# HG changeset patch
# User blanchet
# Date 1335384033 -7200
# Node ID 249a940953b045d26a5c4d46e436d6b784099df6
# Parent  0b2b7ff318675e722dc06949d5bfb2e07cfb1c39
don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."

diff -r 0b2b7ff31867 -r 249a940953b0 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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