src/HOLCF/Porder.ML

 "!!F. is_chain(F) ==> is_tord(range(F))"
  (fn _ =>
         [
         Safe_tac,
         (rtac nat_less_cases 1),
-        (ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);
+        (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
 
 (* ------------------------------------------------------------------------ *)
 (* technical lemmas about lub and is_lub                                    *)
 (* ------------------------------------------------------------------------ *)
 bind_thm("lub",lub_def RS meta_eq_to_obj_eq);

         ]);
 
 
 goal thy "lub{x} = x";
 by (rtac thelubI 1);
-by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
 qed "lub_singleton";
 Addsimps [lub_singleton];
 
 (* ------------------------------------------------------------------------ *)
 (* access to some definition as inference rule                              *)