# HG changeset patch
# User blanchet
# Date 1337800788 -7200
# Node ID 2aea51a142008e76b94c51d954b6467216f224bc
# Parent  257fc09aa8a19b96ad613c9a9014a28692cd9728
generate THF definitions

diff -r 257fc09aa8a1 -r 2aea51a14200 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 17:57:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 21:19:48 2012 +0200
@@ -1297,11 +1297,26 @@
      atomic_types = atomic_Ts}
   end
 
-fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
-  case t |> make_formula ctxt format type_enc iff_for_eq name stature Axiom of
-    formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
-    if s = tptp_true then NONE else SOME formula
-  | formula => SOME formula
+fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    (is_Const t orelse is_Free t) andalso
+    not (exists_subterm (curry (op =) t) u)
+  | is_legitimate_thf_def _ = false
+
+fun make_fact ctxt format type_enc iff_for_eq
+              ((name, stature as (_, status)), t) =
+  let
+    val role =
+      if is_type_enc_higher_order type_enc andalso status = Def andalso
+         is_legitimate_thf_def t then
+        Definition
+      else
+        Axiom
+  in
+    case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
+      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+      if s = tptp_true then NONE else SOME formula
+    | formula => SOME formula
+  end
 
 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
   | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
@@ -2878,8 +2893,7 @@
         else
           I
       | add_eq_deps _ _ = I
-    fun has_status status (_, info) =
-      extract_isabelle_status info = SOME status
+    fun has_status status (_, info) = extract_isabelle_status info = SOME status
     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
       Graph.empty