# HG changeset patch
# User huffman
# Date 1274560056 25200
# Node ID a1fb7947dc2bc00a807596323f702f371bf9ade3
# Parent  3e5146b93218255d50708f6ec5296483155e9904
removed fixrec_simp attribute (cf. a2a1c8a658ef)

diff -r 3e5146b93218 -r a1fb7947dc2b src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat May 22 12:56:33 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat May 22 13:27:36 2010 -0700
@@ -198,7 +198,6 @@
 
 fun qualified name = Binding.qualified true name dbind;
 val simp = Simplifier.simp_add;
-val fixrec_simp = Fixrec.fixrec_simp_add;
 
 in
   thy
@@ -209,7 +208,7 @@
       [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
      ((qualified "when_rews" , when_rews   ), [simp]),
      ((qualified "compacts"  , compacts    ), [simp]),
-     ((qualified "con_rews"  , con_rews    ), [simp, fixrec_simp]),
+     ((qualified "con_rews"  , con_rews    ), [simp]),
      ((qualified "sel_rews"  , sel_rews    ), [simp]),
      ((qualified "dis_rews"  , dis_rews    ), [simp]),
      ((qualified "pat_rews"  , pat_rews    ), [simp]),
@@ -218,7 +217,7 @@
      ((qualified "inverts"   , inverts     ), [simp]),
      ((qualified "injects"   , injects     ), [simp]),
      ((qualified "take_rews" , take_rews   ), [simp]),
-     ((qualified "match_rews", mat_rews    ), [simp, fixrec_simp])]
+     ((qualified "match_rews", mat_rews    ), [simp])]
   |> snd
   |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
       pat_rews @ dist_les @ dist_eqs)