--- a/src/Pure/Proof/reconstruct.ML Tue Jul 19 17:21:46 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jul 19 17:21:47 2005 +0200
@@ -75,7 +75,7 @@
(t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
| SOME T =>
- let val T' = incr_tvar (maxidx + 1) T
+ let val T' = Logic.incr_tvar (maxidx + 1) T
in (Const (s, T'), T', vTs,
Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
end)
@@ -355,7 +355,7 @@
then (maxidx, prfs, prf) else
let
fun inc i =
- map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i);
+ map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
val (maxidx', prf, prfs') =
(case gen_assoc (op =) (prfs, (a, prop)) of
NONE =>