1.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 14:38:25 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed May 19 16:08:41 2010 -0700
     1.3 @@ -952,7 +952,7 @@
     1.4            val (fun1, fun2, taken) = pat_lhs (pat, args);
     1.5            val defs = @{thm branch_def} :: pat_defs;
     1.6            val goal = mk_trp (mk_strict fun1);
     1.7 -          val rules = @{thm Fixrec.bind_strict} :: case_rews;
     1.8 +          val rules = @{thms maybe_when_rews} @ case_rews;
     1.9            val tacs = [simp_tac (beta_ss addsimps rules) 1];
    1.10          in prove thy defs goal (K tacs) end;
    1.11        fun pat_apps (i, (pat, (con, args))) =
    1.12 @@ -967,7 +967,7 @@
    1.13                val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
    1.14                val goal = Logic.list_implies (assms, concl);
    1.15                val defs = @{thm branch_def} :: pat_defs;
    1.16 -              val rules = @{thms bind_fail left_unit} @ case_rews;
    1.17 +              val rules = @{thms maybe_when_rews} @ case_rews;
    1.18                val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
    1.19              in prove thy defs goal (K tacs) end;
    1.20          in map_index pat_app spec end;