Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
don't give weights to built-in symbols
authorblanchet
Thu, 12 May 2011 15:29:19 +0200
changeset 42734 4a1fc1816dbb
parent 42733 01ef1c3d9cfd
child 42735 1d375de437e9
don't give weights to built-in symbols
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle