diff -r 5bfde29f1dbb -r c7fd7eb3b0ef src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:33:39 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:35:20 1999 +0200
@@ -453,12 +453,14 @@
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_localTo_guar_increasing";
 
+(***
 Goal "F : (v LocalTo G) guarantees Increasing func  \
 \     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
 \                         guarantees Increasing (func o sub i)";
 by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_LocalTo_guar_Increasing";
+***)
 
 Goal "F : Always A guarantees Always B \
 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";