Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 48131 1016664b8feb
parent 48130 defbcdc60fd6
child 48143 0186df5074c8 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -717,7 +717,7 @@
                     |> not sound
                        ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
                     |> take num_facts
-                    |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic
+                    |> not (is_type_enc_polymorphic type_enc)
                        ? monomorphize_facts
                     |> map (apsnd prop_of)
                     |> prepare_atp_problem ctxt format prem_role type_enc
isabelle