# HG changeset patch
# User blanchet
# Date 1304337135 -7200
# Node ID 6ef61823b63ba03a5947c720267792384be3aa30
# Parent  c8673078f9153a3eacec4e183e10464723eea389
make sure E type information constants are given a weight, even if they don't appear anywhere else

diff -r c8673078f915 -r 6ef61823b63b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 13:52:15 2011 +0200
@@ -915,6 +915,7 @@
 val hyp_weight = 0.1
 val fact_min_weight = 0.2
 val fact_max_weight = 1.0
+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)
@@ -943,10 +944,14 @@
 
 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
 fun atp_problem_weights problem =
-  Symtab.empty
-  |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
-  |> add_facts_weights (these (AList.lookup (op =) problem factsN))
-  |> Symtab.dest
-  |> sort (prod_ord Real.compare string_ord o pairself swap)
+  let val get = these o AList.lookup (op =) problem in
+    Symtab.empty
+    |> add_conjectures_weights (get free_typesN @ get conjsN)
+    |> add_facts_weights (get factsN)
+    |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
+            [sym_declsN, class_relsN, aritiesN]
+    |> Symtab.dest
+    |> sort (prod_ord Real.compare string_ord o pairself swap)
+  end
 
 end;