src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 57763 e913a87bd5d2
parent 57762 1649841f3b38
child 57765 f1108245ba11
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 19:44:18 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 20:08:50 2014 +0200
@@ -350,7 +350,8 @@
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
-               #> relabel_isar_proof_nicely)
+               #> relabel_isar_proof_nicely
+               #> rename_bound_vars_in_isar_proof)
       in
         (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
           1 =>