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 =>