src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32149 ef59550a55d3
parent 32126 a5042f260440
child 32172 c4e55f30d527
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -685,7 +685,7 @@
     1.4  (* ----- theorems concerning finite approximation and finite induction ------ *)
     1.5  
     1.6  local
     1.7 -  val iterate_Cprod_ss = simpset_of @{theory Fix};
     1.8 +  val iterate_Cprod_ss = global_simpset_of @{theory Fix};
     1.9    val copy_con_rews  = copy_rews @ con_rews;
    1.10    val copy_take_defs =
    1.11      (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;