# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 4a1fc1816dbb56aa0f3a55496107dc5a9368d01b
# Parent  01ef1c3d9cfd7f86afa038fcd8c316e1ad8d03a5
don't give weights to built-in symbols

diff -r 01ef1c3d9cfd -r 4a1fc1816dbb src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -1080,7 +1080,8 @@
 val type_info_default_weight = 0.8
 
 fun add_term_weights weight (ATerm (s, tms)) =
-  (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
+  (not (is_atp_variable s) andalso s <> "equal" andalso
+   not (String.isPrefix "$" s)) ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
     formula_fold true (K (add_term_weights weight)) phi