# HG changeset patch
# User paulson
# Date 830450653 -7200
# Node ID c38d953caedb918e0a5201183424dcc05938b55b
# Parent  2121df6226716bb733a91fa69a55b5444829a577
Fixed some unfortunate variable names

diff -r 2121df622671 -r c38d953caedb src/HOL/ex/Comb.ML
--- a/src/HOL/ex/Comb.ML	Thu Apr 25 17:31:07 1996 +0200
+++ b/src/HOL/ex/Comb.ML	Thu Apr 25 18:44:13 1996 +0200
@@ -47,9 +47,6 @@
 
 (*** Results about Contraction ***)
 
-bind_thm ("contract_induct",
-    (contract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
-
 (** Non-contraction results **)
 
 (*Derive a case for each combinator constructor*)
@@ -122,16 +119,16 @@
 
 (*** Basic properties of parallel contraction ***)
 
-goal Comb.thy "!!x z. K#x =1=> z ==> (EX p'. z = K#p' & x =1=> p')";
+goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
 by (fast_tac parcontract_cs 1);
 qed "K1_parcontractD";
 
-goal Comb.thy "!!x z. S#x =1=> z ==> (EX p'. z = S#p' & x =1=> p')";
+goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
 by (fast_tac parcontract_cs 1);
 qed "S1_parcontractD";
 
 goal Comb.thy
- "!!x y z. S#x#y =1=> z ==> (EX p' q'. z = S#p'#q' & x =1=> p' & y =1=> q')";
+ "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
 by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
      (*the extra rule makes the proof more than twice as fast*)
 qed "S2_parcontractD";