1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 13:09:02 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 13:47:51 2012 +0100
     1.3 @@ -295,6 +295,7 @@
     1.4    By_Metis of facts |
     1.5    Case_Split of isar_step list list * facts
     1.6  
     1.7 +val assume_prefix = "a"
     1.8  val have_prefix = "f"
     1.9  val raw_prefix = "x"
    1.10  
    1.11 @@ -706,24 +707,24 @@
    1.12  val relabel_proof =
    1.13    let
    1.14      fun aux _ _ _ [] = []
    1.15 -      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
    1.16 +      | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
    1.17          if l = no_label then
    1.18 -          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
    1.19 +          Assume (l, t) :: aux subst depth (next_assum, next_have) proof
    1.20          else
    1.21 -          let val l' = (prefix_for_depth depth have_prefix, next_assum) in
    1.22 +          let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
    1.23              Assume (l', t) ::
    1.24 -            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
    1.25 +            aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof
    1.26            end
    1.27 -      | aux subst depth (next_assum, next_fact)
    1.28 +      | aux subst depth (next_assum, next_have)
    1.29              (Prove (qs, l, t, by) :: proof) =
    1.30          let
    1.31 -          val (l', subst, next_fact) =
    1.32 +          val (l', subst, next_have) =
    1.33              if l = no_label then
    1.34 -              (l, subst, next_fact)
    1.35 +              (l, subst, next_have)
    1.36              else
    1.37 -              let
    1.38 -                val l' = (prefix_for_depth depth have_prefix, next_fact)
    1.39 -              in (l', (l, l') :: subst, next_fact + 1) end
    1.40 +              let val l' = (prefix_for_depth depth have_prefix, next_have) in
    1.41 +                (l', (l, l') :: subst, next_have + 1)
    1.42 +              end
    1.43            val relabel_facts =
    1.44              apfst (maps (the_list o AList.lookup (op =) subst))
    1.45            val by =
    1.46 @@ -733,7 +734,7 @@
    1.47                Case_Split (map (aux subst (depth + 1) (1, 1)) proofs,
    1.48                            relabel_facts facts)
    1.49          in
    1.50 -          Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof
    1.51 +          Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof
    1.52          end
    1.53        | aux subst depth nextp (step :: proof) =
    1.54          step :: aux subst depth nextp proof