src/HOLCF/Tools/domain/domain_theorems.ML

                 New proofs/tactics by Brian Huffman
 
 Proof generator for domain command.
 *)
 
-val HOLCF_ss = simpset();
+val HOLCF_ss = @{simpset};
 
 structure Domain_Theorems = struct
 
 local
 

     cut_facts_tac prems 1,
     fast_tac HOL_cs 1]);
 
 val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
   (fn prems =>
-    [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
+    [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
 
 in
 
 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
 let

 val n_eqs = length eqs;
 
 (* ----- theorems concerning finite approximation and finite induction ------ *)
 
 local
-  val iterate_Cprod_ss = simpset_of (theory "Fix");
+  val iterate_Cprod_ss = simpset_of @{theory Fix};
   val copy_con_rews  = copy_rews @ con_rews;
   val copy_take_defs =
     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   val take_stricts =
     let