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_isar_proof.ML
changeset 72401 2783779b7dd3
parent 70586 57df8a85317a
child 72582 b69a3a7655f2 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Oct 08 17:46:03 2020 +0200
@@ -315,7 +315,7 @@
     fun of_method ls ss meth =
       let val direct = is_proof_method_direct meth in
         using_facts ls (if direct then [] else ss) ^
-        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
+        "by " ^ string_of_proof_method (if direct then ss else []) meth
       end
 
     fun of_free (s, T) =
isabelle