--- 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
--- 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