diff -r 3ae9fe3c0f68 -r bca91b4e1710 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cfun3.ML	Wed Oct 04 14:01:44 1995 +0100
@@ -224,7 +224,7 @@
 	"Istrictify(f)(UU)= (UU)"
  (fn prems =>
 	[
-	(simp_tac HOL_ss 1)
+	(Simp_tac 1)
 	]);
 
 qed_goalw "Istrictify2" Cfun3.thy [Istrictify_def]
@@ -232,7 +232,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac HOL_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "monofun_Istrictify1" Cfun3.thy "monofun(Istrictify)"
@@ -384,16 +384,14 @@
 (* Instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-val Cfun_rews  = [minimal,refl_less,beta_cfun,strict_fapp1,strictify1,
-		strictify2];
+Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
+
 
 (* ------------------------------------------------------------------------ *)
 (* use cont_tac as autotac.                                                *)
 (* ------------------------------------------------------------------------ *)
 
-val Cfun_ss = HOL_ss 
-	addsimps  Cfun_rews 
-	setsolver 
-	(fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
-		    (fn i => DEPTH_SOLVE_1 (cont_tac i))
-	);
+simpset := !simpset setsolver 
+           (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
+                       (fn i => DEPTH_SOLVE_1 (cont_tac i))
+           );