1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 08:45:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:41:16 2012 +0200
     1.3 @@ -68,11 +68,13 @@
     1.4  fun mk_pointfree_expr t =
     1.5    let
     1.6      val (vs, t'') = strip_ex (dest_Collect t)
     1.7 -    val (eq::conjs) = HOLogic.dest_conj t''
     1.8 -    val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
     1.9 -            then snd (HOLogic.dest_eq eq)
    1.10 -            else raise TERM("mk_pointfree_expr", [t]);
    1.11 -    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
    1.12 +    val conjs = HOLogic.dest_conj t''
    1.13 +    val is_the_eq =
    1.14 +      the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs)))
    1.15 +    val SOME eq = find_first is_the_eq conjs
    1.16 +    val f = snd (HOLogic.dest_eq eq)
    1.17 +    val conjs' = filter_out (fn t => eq = t) conjs
    1.18 +    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs'
    1.19      val grouped_mems = AList.group (op =) mems
    1.20      fun mk_grouped_unions (i, T) =
    1.21        case AList.lookup (op =) grouped_mems i of
    1.22 @@ -107,9 +109,8 @@
    1.23  
    1.24  val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
    1.25    THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
    1.26 -  THEN' (TRY o (rtac @{thm conjI}))
    1.27 -  THEN' (TRY o hyp_subst_tac)
    1.28 -  THEN' rtac @{thm refl};
    1.29 +  THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
    1.30 +  THEN' (K (ALLGOALS (TRY o ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
    1.31  
    1.32  val tac =
    1.33    let
    1.34 @@ -125,10 +126,7 @@
    1.35      val subset_tac2 = rtac @{thm subsetI}
    1.36        THEN' dest_image_Sigma_tac
    1.37        THEN' intro_Collect_tac
    1.38 -      THEN' REPEAT_DETERM o
    1.39 -        (rtac @{thm conjI}
    1.40 -        ORELSE' eresolve_tac @{thms IntD1 IntD2}
    1.41 -        ORELSE' atac);
    1.42 +      THEN' REPEAT_DETERM o (eresolve_tac @{thms IntD1 IntD2} ORELSE' atac);
    1.43    in
    1.44      rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
    1.45    end;