1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat May 22 12:56:33 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat May 22 13:27:36 2010 -0700
     1.3 @@ -198,7 +198,6 @@
     1.4  
     1.5  fun qualified name = Binding.qualified true name dbind;
     1.6  val simp = Simplifier.simp_add;
     1.7 -val fixrec_simp = Fixrec.fixrec_simp_add;
     1.8  
     1.9  in
    1.10    thy
    1.11 @@ -209,7 +208,7 @@
    1.12        [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
    1.13       ((qualified "when_rews" , when_rews   ), [simp]),
    1.14       ((qualified "compacts"  , compacts    ), [simp]),
    1.15 -     ((qualified "con_rews"  , con_rews    ), [simp, fixrec_simp]),
    1.16 +     ((qualified "con_rews"  , con_rews    ), [simp]),
    1.17       ((qualified "sel_rews"  , sel_rews    ), [simp]),
    1.18       ((qualified "dis_rews"  , dis_rews    ), [simp]),
    1.19       ((qualified "pat_rews"  , pat_rews    ), [simp]),
    1.20 @@ -218,7 +217,7 @@
    1.21       ((qualified "inverts"   , inverts     ), [simp]),
    1.22       ((qualified "injects"   , injects     ), [simp]),
    1.23       ((qualified "take_rews" , take_rews   ), [simp]),
    1.24 -     ((qualified "match_rews", mat_rews    ), [simp, fixrec_simp])]
    1.25 +     ((qualified "match_rews", mat_rews    ), [simp])]
    1.26    |> snd
    1.27    |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    1.28        pat_rews @ dist_les @ dist_eqs)