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) =