--- a/src/Pure/proofterm.ML Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/proofterm.ML Mon Mar 23 19:43:03 2015 +0100
@@ -834,7 +834,7 @@
fun lift_proof Bi inc prop prf =
let
fun lift'' Us Ts t =
- strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
+ strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
fun lift' Us Ts (Abst (s, T, prf)) =
(Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
@@ -878,7 +878,7 @@
fun incr_indexes i =
Same.commit (map_proof_terms_same
- (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
+ (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
(***** proof by assumption *****)