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_tactics.ML
changeset 81610 ed9ffd8e9e40
parent 77418 a8458f0df4ee 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Wed Dec 11 12:04:27 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Wed Dec 18 10:21:58 2024 +0100
@@ -45,7 +45,8 @@
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
+       factss = [("", facts)], has_already_found_something = K false, found_something = K (),
+       memoize_fun_call = (fn f => f)}
     val slice = hd (get_slices ctxt name)
   in
     (case prover params problem slice of
isabelle