src/HOLCF/Sprod3.ML

 qed_goalw "beta_cfun_sprod" thy [spair_def]
         "(LAM x y. Ispair x y)`a`b = Ispair a b"
  (fn prems =>
         [
         (stac beta_cfun 1),
-        (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,
+        (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1,
 					cont2cont_CF1L]) 1),
         (stac beta_cfun 1),
         (rtac cont_Ispair2 1),
         (rtac refl 1)
         ]);