diff -r 4f9c8503d1c5 -r 516f9e349a16 src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Wed Feb 08 11:30:00 1995 +0100
+++ b/src/HOLCF/Cprod1.ML	Wed Feb 15 20:02:47 1995 +0100
@@ -69,7 +69,7 @@
 	[
 	(res_inst_tac [("p","p")] PairE 1),
 	(hyp_subst_tac 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(simp_tac Cfun_ss 1)
 	]);
 
@@ -105,7 +105,7 @@
 	(dtac less_cprod2c 1),
 	(dtac less_cprod2c 1),
 	(rtac (less_cprod1b RS ssubst) 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(etac conjE 1),
 	(etac conjE 1),
 	(rtac conjI 1),