# HG changeset patch
# User huffman
# Date 1267532346 28800
# Node ID 9ed6a6d6615bd1092755231675eae0f8e80f2d41
# Parent  dc59e781669fba29dd986eed99447faa7d902d87
add missing rule to case_strict proof script

diff -r dc59e781669f -r 9ed6a6d6615b src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 02:28:45 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 04:19:06 2010 -0800
@@ -493,7 +493,8 @@
       let
         val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}];
         val goal = mk_trp (mk_strict case_app);
-        val tacs = [resolve_tac @{thms sscase1 ssplit1 strictify1} 1];
+        val rules = @{thms sscase1 ssplit1 strictify1 one_when1};
+        val tacs = [resolve_tac rules 1];
       in prove thy defs goal (K tacs) end;
         
     (* prove rewrites for case combinator *)