1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:33 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:35 2012 +0200
     1.3 @@ -130,6 +130,8 @@
     1.4    | mk_formula (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula t1) (mk_formula t2)
     1.5    | mk_formula t = apfst single (mk_atom t)
     1.6  
     1.7 +fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2) 
     1.8 +  | strip_Int fm = [fm]
     1.9  
    1.10  (* term construction *)
    1.11  
    1.12 @@ -208,12 +210,6 @@
    1.13    THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
    1.14    THEN' hyp_subst_tac
    1.15  
    1.16 -val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
    1.17 -  THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
    1.18 -  THEN' (TRY o (rtac @{thm conjI}))
    1.19 -  THEN' (TRY o hyp_subst_tac)
    1.20 -  THEN' rtac @{thm refl};
    1.21 -
    1.22  fun tac1_of_formula (Int (fm1, fm2)) =
    1.23      TRY o etac @{thm conjE}
    1.24      THEN' rtac @{thm IntI}
    1.25 @@ -255,8 +251,12 @@
    1.26        THEN' (tac1_of_formula fm)
    1.27      val subset_tac2 = rtac @{thm subsetI}
    1.28        THEN' elim_image_tac
    1.29 -      THEN' intro_Collect_tac
    1.30 -      THEN' tac2_of_formula fm
    1.31 +      THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
    1.32 +      THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
    1.33 +      THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
    1.34 +      THEN' (K (SOMEGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))
    1.35 +      THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
    1.36 +        REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula f (i + j)) (strip_Int fm))))
    1.37    in
    1.38      rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
    1.39    end;