src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33427 3182812d33ed
parent 33396 45c5c3c51918
child 33504 b4210cc3ac97
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Nov 03 17:09:27 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Nov 03 18:32:30 2009 -0800
     1.3 @@ -640,7 +640,8 @@
     1.4          ((Binding.name "casedist"  , [casedist]  ), [Induct.cases_type dname]),
     1.5          ((Binding.name "when_rews" , when_rews   ), [Simplifier.simp_add]),
     1.6          ((Binding.name "compacts"  , con_compacts), [Simplifier.simp_add]),
     1.7 -        ((Binding.name "con_rews"  , con_rews    ), [Simplifier.simp_add]),
     1.8 +        ((Binding.name "con_rews"  , con_rews    ),
     1.9 +         [Simplifier.simp_add, Fixrec.fixrec_simp_add]),
    1.10          ((Binding.name "sel_rews"  , sel_rews    ), [Simplifier.simp_add]),
    1.11          ((Binding.name "dis_rews"  , dis_rews    ), [Simplifier.simp_add]),
    1.12          ((Binding.name "pat_rews"  , pat_rews    ), [Simplifier.simp_add]),
    1.13 @@ -649,7 +650,8 @@
    1.14          ((Binding.name "inverts"   , inverts     ), [Simplifier.simp_add]),
    1.15          ((Binding.name "injects"   , injects     ), [Simplifier.simp_add]),
    1.16          ((Binding.name "copy_rews" , copy_rews   ), [Simplifier.simp_add]),
    1.17 -        ((Binding.name "match_rews", mat_rews    ), [Simplifier.simp_add])]
    1.18 +        ((Binding.name "match_rews", mat_rews    ),
    1.19 +         [Simplifier.simp_add, Fixrec.fixrec_simp_add])]
    1.20      |> Sign.parent_path
    1.21      |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    1.22          pat_rews @ dist_les @ dist_eqs @ copy_rews)