# 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