1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Thu May 24 17:46:35 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Thu May 24 18:21:54 2012 +0200
     1.3 @@ -75,8 +75,13 @@
     1.4    let
     1.5      val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 -    val defs = defs |> map (ATP_Util.abs_extensionalize_term ctxt
     1.8 -                            #> aptrueprop (open_form I))
     1.9 +    val (defs, pseudo_defs) =
    1.10 +      defs |> map (ATP_Util.abs_extensionalize_term ctxt
    1.11 +                   #> aptrueprop (open_form I))
    1.12 +           |> List.partition (ATP_Util.is_legitimate_tptp_def
    1.13 +                              o perhaps (try HOLogic.dest_Trueprop)
    1.14 +                              o ATP_Util.unextensionalize_def)
    1.15 +    val nondefs = pseudo_defs @ nondefs
    1.16      val state = Proof.init ctxt
    1.17      val params =
    1.18        [("card", "1\<emdash>100"),

     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 17:46:35 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 18:21:54 2012 +0200
     2.3 @@ -1247,20 +1247,6 @@
     2.4        | freeze t = t
     2.5    in t |> exists_subterm is_Var t ? freeze end
     2.6  
     2.7 -fun unextensionalize_def t =
     2.8 -  case t of
     2.9 -    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
    2.10 -    (case strip_comb lhs of
    2.11 -       (c as Const (_, T), args) =>
    2.12 -       if forall is_Var args andalso not (has_duplicates (op =) args) then
    2.13 -         @{const Trueprop}
    2.14 -         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
    2.15 -            $ c $ fold_rev lambda args rhs)
    2.16 -       else
    2.17 -         t
    2.18 -     | _ => t)
    2.19 -  | _ => t
    2.20 -
    2.21  fun presimp_prop ctxt type_enc t =
    2.22    let
    2.23      val thy = Proof_Context.theory_of ctxt
    2.24 @@ -1296,17 +1282,12 @@
    2.25       atomic_types = atomic_Ts}
    2.26    end
    2.27  
    2.28 -fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    2.29 -    (is_Const t orelse is_Free t) andalso
    2.30 -    not (exists_subterm (curry (op =) t) u)
    2.31 -  | is_legitimate_thf_def _ = false
    2.32 -
    2.33  fun make_fact ctxt format type_enc iff_for_eq
    2.34                ((name, stature as (_, status)), t) =
    2.35    let
    2.36      val role =
    2.37        if is_type_enc_higher_order type_enc andalso status = Def andalso
    2.38 -         is_legitimate_thf_def t then
    2.39 +         is_legitimate_tptp_def t then
    2.40          Definition
    2.41        else
    2.42          Axiom
    2.43 @@ -1329,7 +1310,7 @@
    2.44            let
    2.45              val role =
    2.46                if is_type_enc_higher_order type_enc andalso
    2.47 -                 role <> Conjecture andalso is_legitimate_thf_def t then
    2.48 +                 role <> Conjecture andalso is_legitimate_tptp_def t then
    2.49                  Definition
    2.50                else
    2.51                  role

     3.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu May 24 17:46:35 2012 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu May 24 18:21:54 2012 +0200
     3.3 @@ -38,6 +38,8 @@
     3.4    val eta_expand : typ list -> term -> int -> term
     3.5    val cong_extensionalize_term : theory -> term -> term
     3.6    val abs_extensionalize_term : Proof.context -> term -> term
     3.7 +  val unextensionalize_def : term -> term
     3.8 +  val is_legitimate_tptp_def : term -> bool
     3.9    val transform_elim_prop : term -> term
    3.10    val specialize_type : theory -> (string * typ) -> term -> term
    3.11    val strip_subgoal :
    3.12 @@ -320,6 +322,26 @@
    3.13    else
    3.14      t
    3.15  
    3.16 +fun unextensionalize_def t =
    3.17 +  case t of
    3.18 +    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
    3.19 +    (case strip_comb lhs of
    3.20 +       (c as Const (_, T), args) =>
    3.21 +       if forall is_Var args andalso not (has_duplicates (op =) args) then
    3.22 +         @{const Trueprop}
    3.23 +         $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
    3.24 +            $ c $ fold_rev lambda args rhs)
    3.25 +       else
    3.26 +         t
    3.27 +     | _ => t)
    3.28 +  | _ => t
    3.29 +
    3.30 +fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
    3.31 +  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    3.32 +    (is_Const t orelse is_Free t) andalso
    3.33 +    not (exists_subterm (curry (op =) t) u)
    3.34 +  | is_legitimate_tptp_def _ = false
    3.35 +
    3.36  (* Converts an elim-rule into an equivalent theorem that does not have the
    3.37     predicate variable. Leaves other theorems unchanged. We simply instantiate
    3.38     the conclusion variable to "False". (Cf. "transform_elim_theorem" in