1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 20 17:00:49 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 20 18:08:01 2013 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4  
     1.5    val add_proof_steps : isar_step list -> int -> int
     1.6  
     1.7 -  (** canonical proof labels: 1, 2, 3, ... in post traversal order **)
     1.8 +  (** canonical proof labels: 1, 2, 3, ... in postorder **)
     1.9    val canonical_label_ord : (label * label) -> order
    1.10    val relabel_proof_canonically : isar_proof -> isar_proof
    1.11  
    1.12 @@ -73,7 +73,7 @@
    1.13  struct
    1.14  
    1.15  type label = string * int
    1.16 -type facts = label list * string list (* local & global facts *)
    1.17 +type facts = label list * string list (* local and global facts *)
    1.18  
    1.19  datatype isar_qualifier = Show | Then
    1.20  
    1.21 @@ -160,10 +160,8 @@
    1.22  
    1.23  fun relabel_proof_canonically proof =
    1.24    let
    1.25 -    val lbl = pair ""
    1.26 -
    1.27      fun next_label l (next, subst) =
    1.28 -      (lbl next, (next + 1, (l, lbl next) :: subst))
    1.29 +      let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
    1.30  
    1.31      fun do_byline by (_, subst) =
    1.32        by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the)))
    1.33 @@ -185,13 +183,13 @@
    1.34  
    1.35      and do_step (step as Let _) state = (step, state)
    1.36        | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
    1.37 -      let
    1.38 -        val by = do_byline by state
    1.39 -        val (subproofs, state) = fold_map do_proof subproofs state
    1.40 -        val (l, state) = next_label l state
    1.41 -      in
    1.42 -        (Prove (qs, fix, l, t, subproofs, by), state)
    1.43 -      end
    1.44 +        let
    1.45 +          val by = do_byline by state
    1.46 +          val (subproofs, state) = fold_map do_proof subproofs state
    1.47 +          val (l, state) = next_label l state
    1.48 +        in
    1.49 +          (Prove (qs, fix, l, t, subproofs, by), state)
    1.50 +        end
    1.51    in
    1.52      fst (do_proof proof (0, []))
    1.53    end