# HG changeset patch
# User wenzelm
# Date 1130531278 -7200
# Node ID 5dadabde8fe47583d77fd9e93d24ca5142e65d80
# Parent  19f1ad18bece2e5775a7fa6fbd1116ca4b2fe604
Logic.lift_all;

diff -r 19f1ad18bece -r 5dadabde8fe4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 28 22:27:57 2005 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 28 22:27:58 2005 +0200
@@ -624,8 +624,6 @@
 
 fun lift_proof Bi inc prop prf =
   let
-    val (_, lift_all) = Logic.lift_fns (Bi, inc);
-
     fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
 
     fun lift' Us Ts (Abst (s, T, prf)) =
@@ -645,7 +643,7 @@
       | lift' _ _ _ = raise SAME
     and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
 
-    val ps = map lift_all (Logic.strip_imp_prems prop);
+    val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
     val k = length ps;
 
     fun mk_app (b, (i, j, prf)) =