src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
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
           "" =>