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_mash.ML
changeset 51005 ce4290c33d73
parent 51004 5f2788c38127
child 51007 4f694d52bf62 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -532,7 +532,7 @@
   let
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
-       facts = facts |> map Untranslated_Fact}
+       facts = facts}
   in
     get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
                                problem
isabelle