src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 42183 173b0f488428
parent 42182 a630978fc967
child 42190 b6b5846504cd
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 14:02:03 2011 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4          val (mono_facts, ctxt') =
     1.5            ctxt |> Config.put SMT_Config.verbose debug
     1.6                 |> Config.put SMT_Config.monomorph_limit monomorphize_limit
     1.7 -               |> SMT_Monomorph.monomorph indexed_facts
     1.8 +               |> SMT_Monomorph.monomorph true indexed_facts
     1.9        in
    1.10          mono_facts
    1.11          |> sort (int_ord o pairself fst)