# HG changeset patch # User desharna # Date 1605175234 -3600 # Node ID 18eb7ec2720f9beb12623456d606c932364c96d4 # Parent 4ea19e5dc67e591c7f310baac8643d24c298434d Tuned indentation diff -r 4ea19e5dc67e -r 18eb7ec2720f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 4ea19e5dc67e -r 18eb7ec2720f src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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