diff -r 89341b897412 -r 7e1a73fc0c8b src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Sep 22 16:30:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Sep 22 16:30:47 2011 +0200
@@ -183,7 +183,7 @@
       else
         conj_clauses @ fact_clauses
         |> map (pair 0)
-        |> rpair ctxt
+        |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)
         |-> Monomorph.monomorph atp_schematic_consts_of
         |> fst |> chop (length conj_clauses)
         |> pairself (maps (map (zero_var_indexes o snd)))