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_run.ML
changeset 42544 75cb06eee990
parent 42542 024920b65ce2
child 42579 2552c09b1a72 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:24 2011 +0200
@@ -250,8 +250,7 @@
               (if monomorphize then
                  K (Untranslated_Fact o fst)
                else
-                 ATP_Translated_Fact
-                 oo K (translate_atp_fact ctxt type_sys false o fst))
+                 ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
               (K (K NONE)) atps
       fun launch_smts accum =
         if null smts then
isabelle