src/HOLCF/Lift2.ML

 (* -------------------------------------------------------------------------*)
 (* type ('a)lift is pointed                                                *)
 (* ------------------------------------------------------------------------ *)
 
 goal Lift2.thy  "Undef << x";
-by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
+by (simp_tac (simpset() addsimps [inst_lift_po]) 1);
 qed"minimal_lift";
 
 bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
 
 qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"

 by (etac spec 1);
 by (rtac sym 1);
 by (etac spec 1); 
 
 by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
-by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
+by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
 by (rtac (chain_mono2_po RS exE) 1); 
 by (Fast_tac 1); 
 by (atac 1); 
 by (res_inst_tac [("x","Suc(x)")] exI 1); 
 by (strip_tac 1);