1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 21:02:14 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Oct 15 16:18:48 2012 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4        T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2
     1.5    end;
     1.6  
     1.7 -fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
     1.8 +fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (x, T, t)) = ((x, T), t)
     1.9    | dest_Collect t = raise TERM ("dest_Collect", [t])
    1.10  
    1.11  (* Copied from predicate_compile_aux.ML *)
    1.12 @@ -151,14 +151,15 @@
    1.13  
    1.14  fun mk_pointfree_expr t =
    1.15    let
    1.16 -    val (vs, t'') = strip_ex (dest_Collect t)
    1.17 +    val ((x, T), (vs, t'')) = apsnd strip_ex (dest_Collect t)
    1.18      val Ts = map snd (rev vs)
    1.19      fun mk_mem_UNIV n = HOLogic.mk_mem (Bound n, HOLogic.mk_UNIV (nth Ts n))
    1.20      fun lookup (pat', t) pat = if pat = pat' then t else HOLogic.mk_UNIV (type_of_pattern Ts pat)
    1.21      val conjs = HOLogic.dest_conj t''
    1.22 +    val refl = HOLogic.eq_const T $ Bound (length vs) $ Bound (length vs)
    1.23      val is_the_eq =
    1.24        the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs)))
    1.25 -    val SOME eq = find_first is_the_eq conjs
    1.26 +    val eq = the_default refl (find_first is_the_eq conjs)
    1.27      val f = snd (HOLogic.dest_eq eq)
    1.28      val conjs' = filter_out (fn t => eq = t) conjs
    1.29      val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
    1.30 @@ -169,7 +170,7 @@
    1.31        | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
    1.32        | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
    1.33      val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
    1.34 -    val t = mk_split_abs (rev vs) pat (reorder_bounds pats f)
    1.35 +    val t = mk_split_abs (rev ((x, T) :: vs)) pat (reorder_bounds pats f)
    1.36    in
    1.37      (fm, mk_image t (mk_set fm))
    1.38    end;
    1.39 @@ -196,7 +197,7 @@
    1.40  val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
    1.41    THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
    1.42    THEN' TRY o etac @{thm conjE}
    1.43 -  THEN' hyp_subst_tac;
    1.44 +  THEN' TRY o hyp_subst_tac;
    1.45  
    1.46  fun intro_image_tac ctxt = rtac @{thm image_eqI}
    1.47      THEN' (REPEAT_DETERM1 o
    1.48 @@ -252,9 +253,9 @@
    1.49      val subset_tac2 = rtac @{thm subsetI}
    1.50        THEN' elim_image_tac
    1.51        THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
    1.52 -      THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
    1.53 +      THEN' REPEAT_DETERM o resolve_tac @{thms exI}
    1.54        THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
    1.55 -      THEN' (K (SOMEGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))
    1.56 +      THEN' (K (TRY (SOMEGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
    1.57        THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
    1.58          REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula f (i + j)) (strip_Int fm))))
    1.59    in