# HG changeset patch
# User huffman
# Date 1119047607 -7200
# Node ID 8ebc8f530ab4744d465f30c8c28976c7fbfca993
# Parent  e6b431cb8e0c5874f32e2b0b2f5ea26596379d88
make match_rews into simp rules by default

diff -r e6b431cb8e0c -r 8ebc8f530ab4 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Fri Jun 17 21:19:31 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML	Sat Jun 18 00:33:27 2005 +0200
@@ -331,12 +331,12 @@
 		("con_rews", con_rews),
 		("sel_rews", sel_rews),
 		("dis_rews", dis_rews),
-		("match_rews", mat_rews),
 		("dist_les", dist_les),
 		("dist_eqs", dist_eqs),
 		("inverts" , inverts ),
 		("injects" , injects ),
 		("copy_rews", copy_rews)])))
+       |> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
        |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
                  dist_les @ dist_eqs @ copy_rews)
 end; (* let *)