# HG changeset patch
# User huffman
# Date 1267470918 28800
# Node ID eb0fd03d34f9212203a72d3ecb800b0a5f63e75d
# Parent  d1630f317ed05fae645ffdf6ada9d07557ee0c5c
add missing strictify rule to proof script

diff -r d1630f317ed0 -r eb0fd03d34f9 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 10:00:14 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 11:15:18 2010 -0800
@@ -507,7 +507,7 @@
           val concl = mk_trp (mk_eq (lhs, rhs));
           val goal = Logic.list_implies (assms, concl);
           val defs = case_beta :: con_betas;
-          val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1};
+          val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
           val rules2 = @{thms con_defined_iff_rules};
           val rules3 = @{thms cfcomp2 one_when2};
           val rules = abs_inverse :: rules1 @ rules2 @ rules3;