--- a/src/HOL/Lambda/Lambda.ML Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/Lambda/Lambda.ML Fri Feb 09 13:41:59 1996 +0100
@@ -102,7 +102,7 @@
by (excluded_middle_tac "nat < i" 1);
by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
-bind_thm("lift_lift", result() RS spec RS spec RS mp);
+qed_spec_mp "lift_lift";
goal Lambda.thy "!i j s. j < Suc i --> \
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
@@ -171,7 +171,7 @@
by (Asm_simp_tac 1);
by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
-bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp);
+qed_spec_mp "subst_subst";
(*** Equivalence proof for optimized substitution ***)