1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 17:46:35 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 18:21:54 2012 +0200
     1.3 @@ -1247,20 +1247,6 @@
     1.4        | freeze t = t
     1.5    in t |> exists_subterm is_Var t ? freeze end
     1.6  
     1.7 -fun unextensionalize_def t =
     1.8 -  case t of
     1.9 -    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
    1.10 -    (case strip_comb lhs of
    1.11 -       (c as Const (_, T), args) =>
    1.12 -       if forall is_Var args andalso not (has_duplicates (op =) args) then
    1.13 -         @{const Trueprop}
    1.14 -         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
    1.15 -            $ c $ fold_rev lambda args rhs)
    1.16 -       else
    1.17 -         t
    1.18 -     | _ => t)
    1.19 -  | _ => t
    1.20 -
    1.21  fun presimp_prop ctxt type_enc t =
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24 @@ -1296,17 +1282,12 @@
    1.25       atomic_types = atomic_Ts}
    1.26    end
    1.27  
    1.28 -fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    1.29 -    (is_Const t orelse is_Free t) andalso
    1.30 -    not (exists_subterm (curry (op =) t) u)
    1.31 -  | is_legitimate_thf_def _ = false
    1.32 -
    1.33  fun make_fact ctxt format type_enc iff_for_eq
    1.34                ((name, stature as (_, status)), t) =
    1.35    let
    1.36      val role =
    1.37        if is_type_enc_higher_order type_enc andalso status = Def andalso
    1.38 -         is_legitimate_thf_def t then
    1.39 +         is_legitimate_tptp_def t then
    1.40          Definition
    1.41        else
    1.42          Axiom
    1.43 @@ -1329,7 +1310,7 @@
    1.44            let
    1.45              val role =
    1.46                if is_type_enc_higher_order type_enc andalso
    1.47 -                 role <> Conjecture andalso is_legitimate_thf_def t then
    1.48 +                 role <> Conjecture andalso is_legitimate_tptp_def t then
    1.49                  Definition
    1.50                else
    1.51                  role