# HG changeset patch
# User blanchet
# Date 1384967281 -3600
# Node ID 3cad06ff414b877698b165adaf086829a143bb6c
# Parent  05738b7d8191d7d6e14c27185cbdd44e6a8050f8
tuning

diff -r 05738b7d8191 -r 3cad06ff414b src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 20 17:00:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 20 18:08:01 2013 +0100
@@ -61,7 +61,7 @@
 
   val add_proof_steps : isar_step list -> int -> int
 
-  (** canonical proof labels: 1, 2, 3, ... in post traversal order **)
+  (** canonical proof labels: 1, 2, 3, ... in postorder **)
   val canonical_label_ord : (label * label) -> order
   val relabel_proof_canonically : isar_proof -> isar_proof
 
@@ -73,7 +73,7 @@
 struct
 
 type label = string * int
-type facts = label list * string list (* local & global facts *)
+type facts = label list * string list (* local and global facts *)
 
 datatype isar_qualifier = Show | Then
 
@@ -160,10 +160,8 @@
 
 fun relabel_proof_canonically proof =
   let
-    val lbl = pair ""
-
     fun next_label l (next, subst) =
-      (lbl next, (next + 1, (l, lbl next) :: subst))
+      let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
 
     fun do_byline by (_, subst) =
       by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the)))
@@ -185,13 +183,13 @@
 
     and do_step (step as Let _) state = (step, state)
       | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
-      let
-        val by = do_byline by state
-        val (subproofs, state) = fold_map do_proof subproofs state
-        val (l, state) = next_label l state
-      in
-        (Prove (qs, fix, l, t, subproofs, by), state)
-      end
+        let
+          val by = do_byline by state
+          val (subproofs, state) = fold_map do_proof subproofs state
+          val (l, state) = next_label l state
+        in
+          (Prove (qs, fix, l, t, subproofs, by), state)
+        end
   in
     fst (do_proof proof (0, []))
   end