--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:31:15 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:46:51 2020 +0200
@@ -268,10 +268,8 @@
insert_lemma_in_step lem step @ steps
else
step :: insert_lemma_in_steps lem steps
- and insert_lemma_in_proof lem (Proof {fixes, assumptions, steps}) =
- let val steps' = insert_lemma_in_steps lem steps in
- Proof {fixes = fixes, assumptions = assumptions, steps = steps'}
- end
+ and insert_lemma_in_proof lem (proof as Proof {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