changeset 72585 | 18eb7ec2720f |
parent 72584 | 4ea19e5dc67e |
child 72798 | e732c98b02e6 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 22 15:18:08 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 12 11:00:34 2020 +0100 @@ -282,7 +282,7 @@ else step :: insert_lemma_in_steps lem steps and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = - isar_proof_with_steps proof (insert_lemma_in_steps lem steps) + isar_proof_with_steps proof (insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst