1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 15 11:50:34 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 15 13:06:15 2012 +0200
     1.3 @@ -1240,14 +1240,15 @@
     1.4        | freeze t = t
     1.5    in t |> exists_subterm is_Var t ? freeze end
     1.6  
     1.7 -fun eta_reduce_def t =
     1.8 +fun unextensionalize_def t =
     1.9    case t of
    1.10 -    Const (@{const_name HOL.eq}, _) $ lhs $ rhs =>
    1.11 +    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
    1.12      (case strip_comb lhs of
    1.13         (c as Const (_, T), args) =>
    1.14         if forall is_Var args andalso not (has_duplicates (op =) args) then
    1.15 -         Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
    1.16 -         $ c $ fold_rev lambda args rhs
    1.17 +         @{const Trueprop}
    1.18 +         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
    1.19 +            $ c $ fold_rev lambda args rhs)
    1.20         else
    1.21           t
    1.22       | _ => t)
    1.23 @@ -1262,9 +1263,8 @@
    1.24      val need_trueprop = (fastype_of t = @{typ bool})
    1.25      val is_ho = is_type_enc_higher_order type_enc
    1.26    in
    1.27 -    t |> is_ho ? eta_reduce_def
    1.28 -      |> need_trueprop ? HOLogic.mk_Trueprop
    1.29 -      |> not is_ho ? extensionalize_term ctxt
    1.30 +    t |> need_trueprop ? HOLogic.mk_Trueprop
    1.31 +      |> (if is_ho then unextensionalize_def else extensionalize_term ctxt)
    1.32        |> presimplify_term thy
    1.33        |> HOLogic.dest_Trueprop
    1.34    end
    1.35 @@ -1709,7 +1709,7 @@
    1.36          (if needs_fairly_sound then typed_helper_suffix
    1.37           else untyped_helper_suffix)
    1.38        fun dub_and_inst needs_fairly_sound (th, j) =
    1.39 -        let val t = prop_of th in
    1.40 +        let val t = th |> prop_of in
    1.41            if should_specialize_helper type_enc t then
    1.42              map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
    1.43                  types