src/HOLCF/Cprod3.ML

 	(rtac (monofun_fst RS ch2ch_monofun) 1),
 	(rtac ch2ch_fun 1),
 	(rtac (monofun_pair1 RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac allI 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(rtac sym 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(rtac (lub_const RS thelubI) 1)
 	]);
 
 qed_goal "contlub_pair1" Cprod3.thy "contlub(Pair)"
  (fn prems =>

  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
 	(rtac sym 1),
-	(simp_tac pair_ss 1),
+	(simp_tac prod_ss 1),
 	(rtac (lub_const RS thelubI) 1),
 	(rtac lub_equal 1),
 	(atac 1),
 	(rtac (monofun_snd RS ch2ch_monofun) 1),
 	(rtac (monofun_pair2 RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac allI 1),
-	(simp_tac pair_ss 1)
+	(simp_tac prod_ss 1)
 	]);
 
 qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
  (fn prems =>
 	[

 	[
 	(rtac contlubI 1),
 	(strip_tac 1),
 	(rtac (lub_cprod RS thelubI RS ssubst) 1),
 	(atac 1),
-	(simp_tac pair_ss 1)
+	(simp_tac prod_ss 1)
 	]);
 
 qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
  (fn prems =>
 	[
 	(rtac contlubI 1),
 	(strip_tac 1),
 	(rtac (lub_cprod RS thelubI RS ssubst) 1),
 	(atac 1),
-	(simp_tac pair_ss 1)
+	(simp_tac prod_ss 1)
 	]);
 
 qed_goal "contX_fst" Cprod3.thy "contX(fst)"
 (fn prems =>
 	[

 	[
 	(cut_facts_tac prems 1),
 	(rtac (beta_cfun_cprod RS ssubst) 1),
 	(rtac (beta_cfun RS ssubst) 1),
 	(rtac contX_fst 1),
-	(simp_tac pair_ss  1)
+	(simp_tac prod_ss  1)
 	]);
 
 qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] 
 	"csnd[x#y]=y"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac (beta_cfun_cprod RS ssubst) 1),
 	(rtac (beta_cfun RS ssubst) 1),
 	(rtac contX_snd 1),
-	(simp_tac pair_ss  1)
+	(simp_tac prod_ss  1)
 	]);
 
 qed_goalw "surjective_pairing_Cprod2" Cprod3.thy 
 	[cfst_def,csnd_def,cpair_def] "(cfst[p] # csnd[p]) = p"
  (fn prems =>