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