--- a/src/HOLCF/domain/theorems.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Nov 03 14:06:27 1997 +0100
@@ -373,7 +373,7 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
local
- val iterate_Cprod_ss = simpset_of "Fix"
+ val iterate_Cprod_ss = simpset_of Fix.thy
addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;