# HG changeset patch
# User blanchet
# Date 1304370082 -7200
# Node ID 242bc53b98e5909bba6ac2cc368029b73c19e7d1
# Parent  9dd98edd48c255cf8d7b5b9022c6b10927d6164f
do not declare TPTP built-ins, e.g. $true

diff -r 9dd98edd48c2 -r 242bc53b98e5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 23:01:22 2011 +0200
@@ -811,6 +811,7 @@
 
 fun should_declare_sym type_sys pred_sym s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
+  not (String.isPrefix "$" s) andalso
   (type_sys = Many_Typed orelse not pred_sym)
 
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =