src/HOLCF/Tools/domain/domain_theorems.ML
changeset 26342 0f65fa163304
parent 26336 a0e2b706ce73
child 26343 0dd2eab7b296
     1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Proof generator for domain command.
     1.5  *)
     1.6  
     1.7 -val HOLCF_ss = simpset();
     1.8 +val HOLCF_ss = @{simpset};
     1.9  
    1.10  structure Domain_Theorems = struct
    1.11  
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
    1.15    (fn prems =>
    1.16 -    [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
    1.17 +    [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
    1.18  
    1.19  in
    1.20  
    1.21 @@ -638,7 +638,7 @@
    1.22  (* ----- theorems concerning finite approximation and finite induction ------ *)
    1.23  
    1.24  local
    1.25 -  val iterate_Cprod_ss = simpset_of (theory "Fix");
    1.26 +  val iterate_Cprod_ss = simpset_of @{theory Fix};
    1.27    val copy_con_rews  = copy_rews @ con_rews;
    1.28    val copy_take_defs =
    1.29      (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;