src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49544 24094fa47e0d
parent 49543 53b3c532a082
child 49545 8bb6e2d7346b
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -1495,10 +1495,10 @@
     1.4      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
     1.5  
     1.6  fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
     1.7 -  set_naturals set_incls set_set_inclss =
     1.8 +  set_naturals dtor_set_incls dtor_set_set_inclss =
     1.9    let
    1.10 -    val m = length set_incls;
    1.11 -    val n = length set_set_inclss;
    1.12 +    val m = length dtor_set_incls;
    1.13 +    val n = length dtor_set_set_inclss;
    1.14      val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
    1.15      val in_Jsrel = nth in_Jsrels (i - 1);
    1.16      val if_tac =
    1.17 @@ -1508,13 +1508,13 @@
    1.18            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
    1.19              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
    1.20              etac (set_incl RS @{thm subset_trans})])
    1.21 -        passive_set_naturals set_incls),
    1.22 -        CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
    1.23 +        passive_set_naturals dtor_set_incls),
    1.24 +        CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) =>
    1.25            EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
    1.26              rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    1.27 -            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
    1.28 +            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
    1.29              rtac conjI, rtac refl, rtac refl])
    1.30 -        (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
    1.31 +        (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
    1.32          CONJ_WRAP' (fn conv =>
    1.33            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    1.34            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},