src/HOLCF/domain/theorems.ML
changeset 18728 6790126ab5f6
parent 18688 abf0f018b5ec
child 18972 2905d1805e1e
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  		("inverts" , inverts ),
     1.5  		("injects" , injects ),
     1.6  		("copy_rews", copy_rews)])))
     1.7 -       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
     1.8 +       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add])])
     1.9         |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    1.10                   pat_rews @ dist_les @ dist_eqs @ copy_rews)
    1.11  end; (* let *)