src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46219 426ed18eba43
parent 46217 7b19666f0e3d
child 46244 549755ebf4d2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -2119,9 +2119,8 @@
     1.4  fun ap_curry [_] _ t = t
     1.5    | ap_curry arg_Ts tuple_T t =
     1.6      let val n = length arg_Ts in
     1.7 -      list_abs (map (pair "c") arg_Ts,
     1.8 -                incr_boundvars n t
     1.9 -                $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
    1.10 +      fold_rev (Term.abs o pair "c") arg_Ts
    1.11 +                (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
    1.12      end
    1.13  
    1.14  fun num_occs_of_bound_in_term j (t1 $ t2) =
    1.15 @@ -2182,9 +2181,9 @@
    1.16            val step_body = recs |> map (repair_rec j)
    1.17                                 |> List.foldl s_disj @{const False}
    1.18          in
    1.19 -          (list_abs (tl xs, incr_bv (~1, j, base_body))
    1.20 +          (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
    1.21             |> ap_n_split (length arg_Ts) tuple_T bool_T,
    1.22 -           Abs ("y", tuple_T, list_abs (tl xs, step_body)
    1.23 +           Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
    1.24                                |> ap_n_split (length arg_Ts) tuple_T bool_T))
    1.25          end
    1.26        | aux t =
    1.27 @@ -2235,7 +2234,7 @@
    1.28        image_const $ (rtrancl_const $ step_set) $ base_set
    1.29        |> predicatify tuple_T
    1.30    in
    1.31 -    list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
    1.32 +    fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T)
    1.33      |> unfold_defs_in_term hol_ctxt
    1.34    end
    1.35