changeset 55282 | d4a033f07800 |
parent 55280 | f0187a12b8f2 |
child 55285 | e88ad20035f4 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 13:35:50 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 13:37:23 2014 +0100 @@ -321,7 +321,7 @@ |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> chain_isar_proof ||> kill_useless_labels_in_isar_proof - ||> relabel_isar_proof_finally + ||> relabel_isar_proof_nicely in (case string_of_isar_proof (K (K "")) isar_proof of "" =>