changeset 57792 | 9cb24c835284 |
parent 57791 | d80d3fb56270 |
child 58061 | 3d060f43accb |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 05 10:17:15 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 05 10:59:40 2014 +0200 @@ -361,7 +361,8 @@ ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof - #> relabel_isar_proof_nicely) + #> relabel_isar_proof_nicely + #> rationalize_obtains_in_isar_proofs ctxt) in (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of 1 =>