src/HOLCF/Cprod3.ML

 qed_goalw "beta_cfun_cprod" Cprod3.thy [cpair_def]
         "(LAM x y.(x,y))`a`b = (a,b)"
  (fn prems =>
         [
         (stac beta_cfun 1),
-        (simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
+        (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
         (stac beta_cfun 1),
         (rtac cont_pair2 1),
         (rtac refl 1)
         ]);
 

         "csplit`f`<x,y> = f`x`y"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (Simp_tac 1),
-        (simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
+        (simp_tac (simpset() addsimps [cfst2,csnd2]) 1)
         ]);
 
 qed_goalw "csplit3" Cprod3.thy [csplit_def]
   "csplit`cpair`z=z"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (Simp_tac 1),
-        (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
+        (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for Cprod                                             *)
 (* ------------------------------------------------------------------------ *)