# HG changeset patch
# User desharna
# Date 1642253176 -3600
# Node ID b87fcf474e7f19254e21b09a0e63c7dec7cc3c93
# Parent  a10873b3c7d45bb3fddbe5fe45838177bc0b707d
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer

diff -r a10873b3c7d4 -r b87fcf474e7f src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jan 12 16:33:07 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 15 14:26:16 2022 +0100
@@ -2375,17 +2375,21 @@
     fun var_types () =
       if is_type_enc_polymorphic type_enc then [tvar_a]
       else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
-    fun add_undefined_const T =
-      let
-        val name = `(make_fixed_const NONE) \<^const_name>\<open>undefined\<close>
-        val ((s, s'), Ts) =
-          if is_type_enc_mangling type_enc then
-            (mangled_const_name type_enc [T] name, [])
-          else
-            (name, [T])
-      in
-        Symtab.map_default (s, []) (insert_type thy #3 (s', Ts, T, false, 0, false))
-      end
+    (* Don't add declaration for undefined_bool as bool already has fTrue and fFalse als witnesses
+       and this declaration causes problems in FOF if undefined_bool occurs without predicator pp.
+     *)
+    fun add_undefined_const \<^Type>\<open>bool\<close> = I
+      | add_undefined_const T =
+        let
+          val name = `(make_fixed_const NONE) \<^const_name>\<open>undefined\<close>
+          val ((s, s'), Ts) =
+            if is_type_enc_mangling type_enc then
+              (mangled_const_name type_enc [T] name, [])
+            else
+              (name, [T])
+        in
+          Symtab.map_default (s, []) (insert_type thy #3 (s', Ts, T, false, 0, false))
+        end
     fun add_TYPE_const () =
       let val (s, s') = TYPE_name in
         Symtab.map_default (s, [])