--- 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