add missing rule to case_strict proof script

--- 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 *)