diff -r 30e80f028c57 -r 8129641e90ab Prod.ML
--- a/Prod.ML	Tue May 03 15:48:19 1994 +0200
+++ b/Prod.ML	Fri May 13 11:14:20 1994 +0200
@@ -61,10 +61,10 @@
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
-by(res_inst_tac[("p","s")]PairE 1);
-by(res_inst_tac[("p","t")]PairE 1);
-by(asm_simp_tac pair_ss 1);
-val pair_eq = result();
+by (res_inst_tac[("p","s")] PairE 1);
+by (res_inst_tac[("p","t")] PairE 1);
+by (asm_simp_tac pair_ss 1);
+val Pair_fst_snd_eq = result();
 
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy