src/HOLCF/Tools/domain/domain_theorems.ML
changeset 25132 dffe405b090d
parent 24712 64ed05609568
child 25805 5df82bb5b982
     1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Oct 21 14:21:48 2007 +0200
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Oct 21 14:21:53 2007 +0200
     1.3 @@ -316,14 +316,14 @@
     1.4  
     1.5    fun pat_strict c =
     1.6      let
     1.7 -      val axs = branch_def :: axs_pat_def;
     1.8 +      val axs = @{thm branch_def} :: axs_pat_def;
     1.9        val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
    1.10        val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
    1.11      in pg axs goal tacs end;
    1.12  
    1.13    fun pat_app c (con, args) =
    1.14      let
    1.15 -      val axs = branch_def :: axs_pat_def;
    1.16 +      val axs = @{thm branch_def} :: axs_pat_def;
    1.17        val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
    1.18        val rhs = if con = fst c then pat_rhs c else %%:failN;
    1.19        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));