src/HOLCF/domain/theorems.ML
changeset 4098 71e05eb27fb6
parent 4062 fa2eb95b1b2d
child 4221 ed0f67fb458b
     1.1 --- a/src/HOLCF/domain/theorems.ML	Mon Nov 03 12:36:48 1997 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Nov 03 14:06:27 1997 +0100
     1.3 @@ -373,7 +373,7 @@
     1.4  (* ----- theorems concerning finite approximation and finite induction ------ *)
     1.5  
     1.6  local
     1.7 -  val iterate_Cprod_ss = simpset_of "Fix"
     1.8 +  val iterate_Cprod_ss = simpset_of Fix.thy
     1.9                           addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
    1.10    val copy_con_rews  = copy_rews @ con_rews;
    1.11    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;