Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
drop partial monomorphic instances in Metis, like in Sledgehammer
authorblanchet
Thu, 22 Sep 2011 16:30:47 +0200
changeset 45043 7e1a73fc0c8b
parent 45042 89341b897412
child 45045 7ac79855b1e2
drop partial monomorphic instances in Metis, like in Sledgehammer
src/HOL/Tools/Metis/metis_translate.ML file | annotate | diff | comparison | revisions 
--- 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)))
isabelle