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 prod_ss 1),
+	(Simp_tac 1),
 	(rtac sym 1),
-	(simp_tac prod_ss 1),
+	(Simp_tac 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 prod_ss 1),
+	(Simp_tac 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 prod_ss 1)
+	(Simp_tac 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 prod_ss 1)
+	(Simp_tac 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 prod_ss 1)
+	(Simp_tac 1)
 	]);
 
 qed_goal "cont_fst" Cprod3.thy "cont(fst)"
 (fn prems =>
 	[

 	[
 	(cut_facts_tac prems 1),
 	(rtac (beta_cfun_cprod RS ssubst) 1),
 	(rtac (beta_cfun RS ssubst) 1),
 	(rtac cont_fst 1),
-	(simp_tac prod_ss  1)
+	(Simp_tac  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 cont_snd 1),
-	(simp_tac prod_ss  1)
+	(Simp_tac  1)
 	]);
 
 qed_goalw "surjective_pairing_Cprod2" Cprod3.thy 
 	[cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
  (fn prems =>

 	"csplit`f`<x,y> = f`x`y"
  (fn prems =>
 	[
 	(rtac (beta_cfun RS ssubst) 1),
 	(cont_tacR 1),
-	(simp_tac Cfun_ss 1),
-	(simp_tac (Cfun_ss addsimps [cfst2,csnd2]) 1)
+	(Simp_tac 1),
+	(simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
 	]);
 
 qed_goalw "csplit3" Cprod3.thy [csplit_def]
   "csplit`cpair`z=z"
  (fn prems =>
 	[
 	(rtac (beta_cfun RS ssubst) 1),
 	(cont_tacR 1),
-	(simp_tac (Cfun_ss addsimps [surjective_pairing_Cprod2]) 1)
+	(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for Cprod                                             *)
 (* ------------------------------------------------------------------------ *)
 
-val Cprod_rews = [cfst2,csnd2,csplit2];
-
-val Cprod_ss = Cfun_ss addsimps Cprod_rews;
-
+Addsimps [cfst2,csnd2,csplit2];
+