src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33504 b4210cc3ac97
parent 33427 3182812d33ed
child 33801 e8535acd302c
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:36:30 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:47:00 2009 -0800
     1.3 @@ -589,7 +589,7 @@
     1.4    let
     1.5      val _ = trace " Proving copy_strict...";
     1.6      val goal = mk_trp (strict (dc_copy `% "f"));
     1.7 -    val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
     1.8 +    val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
     1.9      val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    1.10    in pg [ax_copy_def] goal (K tacs) end;
    1.11  
    1.12 @@ -604,9 +604,9 @@
    1.13        val rhs = con_app2 con one_rhs args;
    1.14        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    1.15        val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
    1.16 -      val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
    1.17 +      val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
    1.18        fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
    1.19 -      val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
    1.20 +      val rules = [ax_abs_iso] @ @{thms domain_map_simps};
    1.21        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    1.22      in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    1.23  in