src/HOLCF/Cfun3.ML

         (monofun_Istrictify2 RS monocontlub2cont)); 
 
 
 qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
         (stac beta_cfun 1),
-         (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
 					cont2cont_CF1L]) 1),
         (stac beta_cfun 1),
         (rtac cont_Istrictify2 1),
         (rtac Istrictify1 1)
         ]);
 
 qed_goalw "strictify2" thy [strictify_def]
         "~x=UU ==> strictify`f`x=f`x"  (fn prems => [
         (stac beta_cfun 1),
-         (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+         (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
 					cont2cont_CF1L]) 1),
         (stac beta_cfun 1),
         (rtac cont_Istrictify2 1),
         (rtac Istrictify2 1),
         (resolve_tac prems 1)

 (* ------------------------------------------------------------------------ *)
 (* use cont_tac as autotac.                                                *)
 (* ------------------------------------------------------------------------ *)
 
 (* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
-(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
+(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
 
 (* ------------------------------------------------------------------------ *)
 (* some lemmata for functions with flat/chain_finite domain/range types	    *)
 (* ------------------------------------------------------------------------ *)