# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID cd99d6d3027a1a90ae30f1a033f17e04f010f46e
# Parent  3031d342d5148d9ac97686f9129f3a9e30899de5
reconstruct TFF type predicates correctly for ToFoF

diff -r 3031d342d514 -r cd99d6d3027a src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -346,6 +346,8 @@
             [typ_u, term_u] =>
             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
           | _ => raise FO_TERM us
+        else if String.isPrefix type_prefix a then
+          @{const True} (* ignore TFF type information *)
         else case strip_prefix_and_unascii const_prefix a of
           SOME "equal" =>
           let val ts = map (aux NONE []) us in
@@ -362,7 +364,7 @@
             else if b = explicit_app_base then
               aux opt_T (nth us 1 :: extra_us) (hd us)
             else if b = type_pred_base then
-              @{const True}
+              @{const True} (* ignore type predicates *)
             else
               let
                 val num_ty_args = num_atp_type_args thy type_sys b
diff -r 3031d342d514 -r cd99d6d3027a src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -24,6 +24,7 @@
   val boolify_base : string
   val explicit_app_base : string
   val type_pred_base : string
+  val type_prefix : string
   val is_type_system_sound : type_system -> bool
   val type_system_types_dangerous_types : type_system -> bool
   val num_atp_type_args : theory -> type_system -> string -> int