# HG changeset patch
# User blanchet
# Date 1337079975 -7200
# Node ID 481e5379c4efedeec7f462c8491729008e0fbe82
# Parent  4e951258204b599a3178b20d1dcb48a830abe29d
imported patch atp_tuning

diff -r 4e951258204b -r 481e5379c4ef src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 15 11:50:34 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 15 13:06:15 2012 +0200
@@ -1240,14 +1240,15 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun eta_reduce_def t =
+fun unextensionalize_def t =
   case t of
-    Const (@{const_name HOL.eq}, _) $ lhs $ rhs =>
+    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
     (case strip_comb lhs of
        (c as Const (_, T), args) =>
        if forall is_Var args andalso not (has_duplicates (op =) args) then
-         Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
-         $ c $ fold_rev lambda args rhs
+         @{const Trueprop}
+         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
+            $ c $ fold_rev lambda args rhs)
        else
          t
      | _ => t)
@@ -1262,9 +1263,8 @@
     val need_trueprop = (fastype_of t = @{typ bool})
     val is_ho = is_type_enc_higher_order type_enc
   in
-    t |> is_ho ? eta_reduce_def
-      |> need_trueprop ? HOLogic.mk_Trueprop
-      |> not is_ho ? extensionalize_term ctxt
+    t |> need_trueprop ? HOLogic.mk_Trueprop
+      |> (if is_ho then unextensionalize_def else extensionalize_term ctxt)
       |> presimplify_term thy
       |> HOLogic.dest_Trueprop
   end
@@ -1709,7 +1709,7 @@
         (if needs_fairly_sound then typed_helper_suffix
          else untyped_helper_suffix)
       fun dub_and_inst needs_fairly_sound (th, j) =
-        let val t = prop_of th in
+        let val t = th |> prop_of in
           if should_specialize_helper type_enc t then
             map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
                 types