src/HOLCF/One.ML

  (fn prems =>
 	[
 	(rtac allI 1),
 	(rtac allI 1),
 	(res_inst_tac [("p","x")] oneE 1),
-	(asm_simp_tac ccc1_ss  1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("p","y")] oneE 1),
-	(asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
-	(asm_simp_tac ccc1_ss  1)
+	(asm_simp_tac (!simpset addsimps dist_less_one) 1),
+	(Asm_simp_tac 1)
 	]);
 
 
 (* ------------------------------------------------------------------------ *)
 (* properties of one_when                                                   *)

 (* ------------------------------------------------------------------------ *)
 
 fun prover s =  prove_goalw One.thy [one_when_def,one_def] s
  (fn prems =>
 	[
-	(simp_tac (ccc1_ss addsimps [(rep_one_iso ),
+	(simp_tac (!simpset addsimps [(rep_one_iso ),
 	(abs_one_iso RS allI) RS ((rep_one_iso RS allI) 
 	RS iso_strict) RS conjunct1] )1)
 	]);
 
 val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];