# HG changeset patch
# User blanchet
# Date 1391431043 -3600
# Node ID d4a033f07800083af29620812aa2d15e1a243125
# Parent  765555d6a0b29fff154193921793dd304c41c926
tuning

diff -r 765555d6a0b2 -r d4a033f07800 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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
           "" =>
diff -r 765555d6a0b2 -r d4a033f07800 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 13:35:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 13:37:23 2014 +0100
@@ -56,7 +56,7 @@
   val chain_isar_proof : isar_proof -> isar_proof
   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
   val relabel_isar_proof_canonically : isar_proof -> isar_proof
-  val relabel_isar_proof_finally : isar_proof -> isar_proof
+  val relabel_isar_proof_nicely : isar_proof -> isar_proof
 
   val string_of_isar_proof : Proof.context -> int -> int ->
     (label -> proof_method list -> string) -> isar_proof -> string
@@ -210,7 +210,7 @@
 val assume_prefix = "a"
 val have_prefix = "f"
 
-val relabel_isar_proof_finally =
+val relabel_isar_proof_nicely =
   let
     fun next_label depth prefix l (accum as (next, subst)) =
       if l = no_label then