src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 42181 8f25605e646c
parent 42180 a6c141925a8a
child 42182 a630978fc967
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:53 2011 +0200
     1.3 @@ -348,12 +348,20 @@
     1.4          val facts = facts |> map untranslated_fact
     1.5          val indexed_facts =
     1.6            (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts)
     1.7 +        val (mono_facts, ctxt') =
     1.8 +          ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
     1.9 +               |> SMT_Monomorph.monomorph indexed_facts
    1.10        in
    1.11 -        ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
    1.12 -             |> SMT_Monomorph.monomorph indexed_facts |> fst
    1.13 -             |> sort (int_ord o pairself fst)
    1.14 -             |> filter_out (curry (op =) ~1 o fst)
    1.15 -             |> map (Untranslated_Fact o apfst (fst o nth facts))
    1.16 +        mono_facts
    1.17 +        |> sort (int_ord o pairself fst)
    1.18 +        |> filter_out (curry (op =) ~1 o fst)
    1.19 +        (* The next step shouldn't be necessary but currently the monomorphizer
    1.20 +           generates unexpected instances with fresh TFrees, which typically
    1.21 +           become TVars once exported. *)
    1.22 +        |> filter_out (Term.exists_type SMT_Monomorph.typ_has_tvars
    1.23 +                       o singleton (Variable.export_terms ctxt' ctxt)
    1.24 +                       o prop_of o snd)
    1.25 +        |> map (Untranslated_Fact o apfst (fst o nth facts))
    1.26        end
    1.27      val facts = facts |> monomorphize ? monomorphize_facts
    1.28                        |> map (atp_translated_fact ctxt)