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 57735 056a55b44ec7
parent 57662 cffd1d6ae1e5
child 57757 a30a3d5aaec2 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -814,7 +814,7 @@
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
        subgoal_count = 1, factss = [("", facts)]}
   in
-    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem
+    get_minimizing_prover ctxt MaSh (K ()) prover params problem
   end
 
 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
isabelle