--- 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