--- 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Nov 12 11:00:34 2020 +0100
@@ -208,7 +208,7 @@
| chain_isar_steps prev (i :: is) =
chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
and chain_isar_proof (proof as Proof {assumptions, steps, ...}) =
- isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps)
+ isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps)
fun kill_useless_labels_in_isar_proof proof =
let