# HG changeset patch
# User blanchet
# Date 1301563014 -7200
# Node ID a630978fc96758053212332ce7537c50189c0d16
# Parent  8f25605e646c38e5b95b3c3c95d54bc6d61005b4
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)

diff -r 8f25605e646c -r a630978fc967 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:53 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:54 2011 +0200
@@ -341,15 +341,20 @@
          : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
+    val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     fun monomorphize_facts facts =
       let
         val facts = facts |> map untranslated_fact
+        (* pseudo-theorem involving the same constants as the subgoal *)
+        val subgoal_th =
+          Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
         val indexed_facts =
-          (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts)
+          (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
         val (mono_facts, ctxt') =
-          ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
+          ctxt |> Config.put SMT_Config.verbose debug
+               |> Config.put SMT_Config.monomorph_limit monomorphize_limit
                |> SMT_Monomorph.monomorph indexed_facts
       in
         mono_facts