src/HOL/Tools/ATP/atp_proof_reconstruct.ML

         else if s = tptp_not_and then @{term "% P Q. ~ (P & Q)"}
         else if s = tptp_not_or then @{term "% P Q. ~ (P | Q)"}
         else if s = tptp_not then HOLogic.Not
         else if s = tptp_ho_forall then HOLogic.all_const dummyT
         else if s = tptp_ho_exists then HOLogic.exists_const dummyT
+        else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
+        else if s = tptp_hilbert_the then @{term "The"}
         else
           (case unprefix_and_unascii const_prefix s of
             SOME s' =>
             let
               val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const