# HG changeset patch
# User blanchet
# Date 1301656881 -7200
# Node ID 8eed749527b6c72d844fdb403026c5a666202e31
# Parent  906780d5138e848a39cd2dd47cc69bb4e484468a
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428

diff -r 906780d5138e -r 8eed749527b6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 01 12:19:54 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 01 13:21:21 2011 +0200
@@ -346,26 +346,22 @@
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     fun monomorphize_facts facts =
       let
+        val repair_context =
+          Config.put SMT_Config.verbose debug
+          #> Config.put SMT_Config.monomorph_full false
+          #> Config.put SMT_Config.monomorph_limit monomorphize_limit
         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, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
-        val (mono_facts, ctxt') =
-          ctxt |> Config.put SMT_Config.verbose debug
-               |> Config.put SMT_Config.monomorph_limit monomorphize_limit
-               |> SMT_Monomorph.monomorph indexed_facts
+        val mono_facts =
+          SMT_Monomorph.monomorph indexed_facts (repair_context ctxt) |> fst
       in
         mono_facts
         |> sort (int_ord o pairself fst)
         |> filter_out (curry (op =) ~1 o fst)
-        (* The next step shouldn't be necessary but currently the monomorphizer
-           generates unexpected instances with fresh TFrees, which typically
-           become TVars once exported. *)
-        |> filter_out (Term.exists_type SMT_Monomorph.typ_has_tvars
-                       o singleton (Variable.export_terms ctxt' ctxt)
-                       o prop_of o snd)
         |> map (Untranslated_Fact o apfst (fst o nth facts))
       end
     val facts = facts |> monomorphize ? monomorphize_facts
@@ -559,6 +555,7 @@
           else
             I)
       #> Config.put SMT_Config.infer_triggers (!smt_triggers)
+      #> Config.put SMT_Config.monomorph_full false
       #> Config.put SMT_Config.monomorph_limit monomorphize_limit
     val state = state |> Proof.map_context repair_context