# HG changeset patch
# User desharna
# Date 1607604589 -3600
# Node ID f231444e8f9d8fa2c3fdcf87b22aa42b8f92792c
# Parent  4bf5b4f8bd6f19568b197d0ab5fb8124baf11e97
proper handling of true and false in tptp

diff -r 4bf5b4f8bd6f -r f231444e8f9d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 03 18:27:24 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 10 13:49:49 2020 +0100
@@ -1160,40 +1160,43 @@
             fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
             fun handle_fool card x = if card = argc then x else proxy_const ()
           in
-            (case s of
-              "c_False" => IConst (`I tptp_false, T, [])
-            | "c_True" => IConst (`I tptp_true, T, [])
-            | _ =>
-              if top_level then
-                plain_const ()
-              else if is_type_enc_full_higher_order type_enc then
-                (case s of
-                  "c_Not" => IConst (`I tptp_not, T, [])
-                | "c_conj" => IConst (`I tptp_and, T, [])
-                | "c_disj" => IConst (`I tptp_or, T, [])
-                | "c_implies" => IConst (`I tptp_implies, T, [])
-                | "c_All" => tweak_ho_quant tptp_ho_forall T args
-                | "c_Ex" => tweak_ho_quant tptp_ho_exists T args
-                | s =>
-                  if is_tptp_equal s then
-                    tweak_ho_equal T argc
-                  else
-                    plain_const ())
-              else if is_type_enc_fool type_enc then
-                (case s of
-                  "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, []))
-                | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, []))
-                | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, []))
-                | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
-                | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
-                | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
-                | s =>
-                  if is_tptp_equal s then
-                    handle_fool 2 (IConst (`I tptp_equal, T, []))
-                  else
-                    plain_const ())
-              else
-                proxy_const ())
+            if top_level then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | _ => plain_const ())
+            else if is_type_enc_full_higher_order type_enc then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | "c_Not" => IConst (`I tptp_not, T, [])
+              | "c_conj" => IConst (`I tptp_and, T, [])
+              | "c_disj" => IConst (`I tptp_or, T, [])
+              | "c_implies" => IConst (`I tptp_implies, T, [])
+              | "c_All" => tweak_ho_quant tptp_ho_forall T args
+              | "c_Ex" => tweak_ho_quant tptp_ho_exists T args
+              | s =>
+                if is_tptp_equal s then
+                  tweak_ho_equal T argc
+                else
+                  plain_const ())
+            else if is_type_enc_fool type_enc then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, []))
+              | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, []))
+              | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, []))
+              | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
+              | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
+              | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
+              | s =>
+                if is_tptp_equal s then
+                  handle_fool 2 (IConst (`I tptp_equal, T, []))
+                else
+                  plain_const ())
+            else
+              proxy_const ()
           end
          | NONE =>
            if s = tptp_choice then