# HG changeset patch
# User blanchet
# Date 1307450322 -7200
# Node ID 6c3a2c33fc3934e4326e84183fff8e9338a6a785
# Parent  69375eaa90165f94b571f61a3bd057bef0e36b36
prioritize more relevant facts for monomorphization

diff -r 69375eaa9016 -r 6c3a2c33fc39 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:38:42 2011 +0200
@@ -603,9 +603,14 @@
                 val subgoal_th =
                   Logic.list_implies (hyp_ts, concl_t)
                   |> Skip_Proof.make_thm thy
+                val rths =
+                  facts |> chop (length facts div 4)
+                        |>> map (pair 1 o snd)
+                        ||> map (pair 2 o snd)
+                        |> op @
+                        |> cons (0, subgoal_th)
               in
-                Monomorph.monomorph atp_schematic_consts_of
-                    (subgoal_th :: map snd facts |> map (pair 0)) ctxt
+                Monomorph.monomorph atp_schematic_consts_of rths ctxt
                 |> fst |> tl
                 |> curry ListPair.zip (map fst facts)
                 |> maps (fn (name, rths) => map (pair name o snd) rths)