discontinued old-style Term.list_abs in favour of plain Term.abs;
authorwenzelm
Sat Jan 14 21:16:15 2012 +0100 (2012-01-14)
changeset 46219426ed18eba43
parent 46218 ecf6375e2abb
child 46220 663251a395c2
child 46225 d0a2c4a80a00
discontinued old-style Term.list_abs in favour of plain Term.abs;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/record.ML
src/Provers/hypsubst.ML
src/Pure/Isar/auto_bind.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/pattern.ML
src/Pure/term.ML
src/Pure/unify.ML
src/Tools/cong_tac.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -231,12 +231,13 @@
     1.4              let val T = type_of x
     1.5              in if Datatype_Aux.is_rec_type dt then
     1.6                  let val Us = binder_types T
     1.7 -                in list_abs (map (pair "x") Us,
     1.8 -                  Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
     1.9 -                    list_comb (x, map (fn (i, U) =>
    1.10 -                      Const ("Nominal.perm", permT --> U --> U) $
    1.11 -                        (Const ("List.rev", permT --> permT) $ pi) $
    1.12 -                        Bound i) ((length Us - 1 downto 0) ~~ Us)))
    1.13 +                in
    1.14 +                  fold_rev (Term.abs o pair "x") Us
    1.15 +                    (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
    1.16 +                      list_comb (x, map (fn (i, U) =>
    1.17 +                        Const ("Nominal.perm", permT --> U --> U) $
    1.18 +                          (Const ("List.rev", permT --> permT) $ pi) $
    1.19 +                          Bound i) ((length Us - 1 downto 0) ~~ Us)))
    1.20                  end
    1.21                else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
    1.22              end;
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 20:05:58 2012 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 21:16:15 2012 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4      val Ts = map snd ps;
     2.5      val tinst' = map (fn (t, u) =>
     2.6        (head_of (Logic.incr_indexes (Ts, j) t),
     2.7 -       list_abs (ps, u))) tinst;
     2.8 +       fold_rev Term.abs ps u)) tinst;
     2.9      val th' = instf
    2.10        (map (pairself (ctyp_of thy)) tyinst')
    2.11        (map (pairself (cterm_of thy)) tinst')
    2.12 @@ -155,9 +155,10 @@
    2.13     let val vars' = Misc_Legacy.term_vars (prop_of st);
    2.14         val thy = theory_of_thm st;
    2.15     in case subtract (op =) vars vars' of
    2.16 -     [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    2.17 +     [x] =>
    2.18 +      Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    2.19      | _ => error "fresh_fun_simp: Too many variables, please report."
    2.20 -  end
    2.21 +   end
    2.22    in
    2.23    ((fn st =>
    2.24    let
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Jan 14 20:05:58 2012 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Jan 14 21:16:15 2012 +0100
     3.3 @@ -301,8 +301,8 @@
     3.4              val s = fold_rev (fn v => fn s =>
     3.5                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
     3.6                vs HOLogic.unit;
     3.7 -            val s' = list_abs (ps,
     3.8 -              Const ("Nominal.supp", fastype_of1 (Ts, s) -->
     3.9 +            val s' = fold_rev Term.abs ps
    3.10 +              (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
    3.11                  Term.range_type T) $ s);
    3.12              val supports_rule' = Thm.lift_rule goal supports_rule;
    3.13              val _ $ (_ $ S $ _) =
    3.14 @@ -345,8 +345,9 @@
    3.15              val s = fold_rev (fn v => fn s =>
    3.16                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    3.17                vs HOLogic.unit;
    3.18 -            val s' = list_abs (ps,
    3.19 -              Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
    3.20 +            val s' =
    3.21 +              fold_rev Term.abs ps
    3.22 +                (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
    3.23              val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
    3.24              val _ $ (_ $ S $ _) =
    3.25                Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
     4.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 20:05:58 2012 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 21:16:15 2012 +0100
     4.3 @@ -381,8 +381,8 @@
     4.4                (Logic.mk_implies
     4.5                  (HOLogic.mk_Trueprop (HOLogic.list_all
     4.6                     (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
     4.7 -                 HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
     4.8 -                   r $ (a $ Datatype_Aux.app_bnds f i)), f))))
     4.9 +                 HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
    4.10 +                   (r $ (a $ Datatype_Aux.app_bnds f i)), f))))
    4.11                (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
    4.12                   REPEAT (etac allE 1), rtac thm 1, atac 1])
    4.13            end
     5.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Jan 14 20:05:58 2012 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Jan 14 21:16:15 2012 +0100
     5.3 @@ -345,7 +345,7 @@
     5.4              val (xs, ys) =
     5.5                if j < i then (zs @ map (pair "x") (drop j Us), [])
     5.6                else chop i zs;
     5.7 -            val u = list_abs (ys, strip_abs_body t);
     5.8 +            val u = fold_rev Term.abs ys (strip_abs_body t);
     5.9              val xs' = map Free
    5.10                ((fold_map Name.variant (map fst xs)
    5.11                    (Term.declare_term_names u used) |> fst) ~~
     6.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 20:05:58 2012 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 21:16:15 2012 +0100
     6.3 @@ -235,8 +235,8 @@
     6.4  
     6.5          fun mk_reccomb ((dt, T), t) =
     6.6            let val (Us, U) = strip_type T in
     6.7 -            list_abs (map (pair "x") Us,
     6.8 -              nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
     6.9 +            fold_rev (Term.abs o pair "x") Us
    6.10 +              (nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
    6.11            end;
    6.12  
    6.13          val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees');
     7.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 21:16:15 2012 +0100
     7.3 @@ -216,8 +216,8 @@
     7.4          (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
     7.5      val r' =
     7.6        Logic.varify_global (Abs ("y", T,
     7.7 -        list_abs (map dest_Free rs, list_comb (r,
     7.8 -          map Bound ((length rs - 1 downto 0) @ [length rs])))));
     7.9 +        (fold_rev (Term.abs o dest_Free) rs
    7.10 +          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
    7.11    in
    7.12      Extraction.add_realizers_i
    7.13        [(exh_name, (["P"], r', prf)),
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 20:05:58 2012 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 21:16:15 2012 +0100
     8.3 @@ -2119,9 +2119,8 @@
     8.4  fun ap_curry [_] _ t = t
     8.5    | ap_curry arg_Ts tuple_T t =
     8.6      let val n = length arg_Ts in
     8.7 -      list_abs (map (pair "c") arg_Ts,
     8.8 -                incr_boundvars n t
     8.9 -                $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
    8.10 +      fold_rev (Term.abs o pair "c") arg_Ts
    8.11 +                (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
    8.12      end
    8.13  
    8.14  fun num_occs_of_bound_in_term j (t1 $ t2) =
    8.15 @@ -2182,9 +2181,9 @@
    8.16            val step_body = recs |> map (repair_rec j)
    8.17                                 |> List.foldl s_disj @{const False}
    8.18          in
    8.19 -          (list_abs (tl xs, incr_bv (~1, j, base_body))
    8.20 +          (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
    8.21             |> ap_n_split (length arg_Ts) tuple_T bool_T,
    8.22 -           Abs ("y", tuple_T, list_abs (tl xs, step_body)
    8.23 +           Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
    8.24                                |> ap_n_split (length arg_Ts) tuple_T bool_T))
    8.25          end
    8.26        | aux t =
    8.27 @@ -2235,7 +2234,7 @@
    8.28        image_const $ (rtrancl_const $ step_set) $ base_set
    8.29        |> predicatify tuple_T
    8.30    in
    8.31 -    list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
    8.32 +    fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T)
    8.33      |> unfold_defs_in_term hol_ctxt
    8.34    end
    8.35  
     9.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jan 14 20:05:58 2012 +0100
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jan 14 21:16:15 2012 +0100
     9.3 @@ -436,7 +436,7 @@
     9.4      val bs = map (pair "x") inpTs
     9.5      val bounds = map Bound (rev (0 upto (length bs) - 1))
     9.6      val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
     9.7 -  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
     9.8 +  in fold_rev Term.abs bs (mk_single compfuns (list_comb (f, bounds))) end
     9.9  
    9.10  fun register_alternative_function pred_name mode fun_name =
    9.11    Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 14 20:05:58 2012 +0100
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 14 21:16:15 2012 +0100
    10.3 @@ -703,12 +703,12 @@
    10.4          let
    10.5            val bs = map (pair "x") (binder_types (fastype_of t))
    10.6            val bounds = map Bound (rev (0 upto (length bs) - 1))
    10.7 -        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
    10.8 +        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
    10.9        | (t, Context m) =>
   10.10          let
   10.11            val bs = map (pair "x") (binder_types (fastype_of t))
   10.12            val bounds = map Bound (rev (0 upto (length bs) - 1))
   10.13 -        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
   10.14 +        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
   10.15        | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
   10.16          (case (expr_of (t1, d1), expr_of (t2, d2)) of
   10.17            (NONE, NONE) => NONE
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Jan 14 20:05:58 2012 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Jan 14 21:16:15 2012 +0100
    11.3 @@ -235,10 +235,10 @@
    11.4                              Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
    11.5                            val Ts = binder_types (fastype_of t)
    11.6                          in
    11.7 -                          list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
    11.8 -                            mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
    11.9 -                            HOLogic.mk_eq (@{term True}, Bound 0),
   11.10 -                            HOLogic.mk_eq (@{term False}, Bound 0)))
   11.11 +                          fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})])
   11.12 +                            (mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
   11.13 +                              HOLogic.mk_eq (@{term True}, Bound 0),
   11.14 +                              HOLogic.mk_eq (@{term False}, Bound 0)))
   11.15                          end
   11.16                      val argvs' = map2 lift_arg Ts argvs
   11.17                      val resname = singleton (Name.variant_list names') "res"
    12.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 20:05:58 2012 +0100
    12.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 21:16:15 2012 +0100
    12.3 @@ -462,7 +462,7 @@
    12.4        let
    12.5          val frees = Term.add_frees t []
    12.6          val t' = fold_rev absfree frees t
    12.7 -        fun wrap f t = list_abs (f (strip_abs t))
    12.8 +        fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
    12.9          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   12.10          fun ensure_testable t =
   12.11            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    13.1 --- a/src/HOL/Tools/inductive.ML	Sat Jan 14 20:05:58 2012 +0100
    13.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 21:16:15 2012 +0100
    13.3 @@ -652,9 +652,10 @@
    13.4                  val k = length Ts;
    13.5                  val bs = map Bound (k - 1 downto 0);
    13.6                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
    13.7 -                val Q = list_abs (mk_names "x" k ~~ Ts,
    13.8 -                  HOLogic.mk_binop inductive_conj_name
    13.9 -                    (list_comb (incr_boundvars k s, bs), P));
   13.10 +                val Q =
   13.11 +                  fold_rev Term.abs (mk_names "x" k ~~ Ts)
   13.12 +                    (HOLogic.mk_binop inductive_conj_name
   13.13 +                      (list_comb (incr_boundvars k s, bs), P));
   13.14                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
   13.15            | NONE =>
   13.16                (case s of
   13.17 @@ -760,9 +761,10 @@
   13.18              val l = length Us;
   13.19              val zs = map Bound (l - 1 downto 0);
   13.20            in
   13.21 -            list_abs (map (pair "z") Us, list_comb (p,
   13.22 -              make_bool_args' bs i @ make_args argTs
   13.23 -                ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
   13.24 +            fold_rev (Term.abs o pair "z") Us
   13.25 +              (list_comb (p,
   13.26 +                make_bool_args' bs i @ make_args argTs
   13.27 +                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
   13.28            end
   13.29        | NONE =>
   13.30            (case t of
    14.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
    14.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 21:16:15 2012 +0100
    14.3 @@ -88,8 +88,9 @@
    14.4            val u = list_comb (t, map Bound (i - 1 downto 0))
    14.5          in 
    14.6            if member (op =) vs a then
    14.7 -            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
    14.8 -          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
    14.9 +            fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
   14.10 +          else
   14.11 +            fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
   14.12          end
   14.13    | gen_rvar _ t = t;
   14.14  
   14.15 @@ -164,24 +165,25 @@
   14.16                  let
   14.17                    val prem' :: prems' = prems;
   14.18                    val U = Extraction.etype_of thy vs [] prem';
   14.19 -                in if U = Extraction.nullT
   14.20 +                in
   14.21 +                  if U = Extraction.nullT
   14.22                    then fun_of (Free (x, T) :: ts)
   14.23                      (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   14.24                      (Free (x, T) :: args) (x :: r :: used) prems'
   14.25                    else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
   14.26                      (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
   14.27                  end
   14.28 -              else (case strip_type T of
   14.29 +              else
   14.30 +                (case strip_type T of
   14.31                    (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
   14.32                      let
   14.33                        val fx = Free (x, Ts ---> T1);
   14.34                        val fr = Free (r, Ts ---> T2);
   14.35                        val bs = map Bound (length Ts - 1 downto 0);
   14.36 -                      val t = list_abs (map (pair "z") Ts,
   14.37 -                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
   14.38 -                    in fun_of (fx :: ts) (fr :: rts) (t::args)
   14.39 -                      (x :: r :: used) prems
   14.40 -                    end
   14.41 +                      val t =
   14.42 +                        fold_rev (Term.abs o pair "z") Ts
   14.43 +                          (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
   14.44 +                    in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
   14.45                  | (Ts, U) => fun_of (Free (x, T) :: ts)
   14.46                      (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
   14.47                      (Free (x, T) :: args) (x :: r :: used) prems)
   14.48 @@ -439,13 +441,16 @@
   14.49          val T' = Extraction.etype_of thy (vs @ Ps) [] p;
   14.50          val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
   14.51          val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
   14.52 -        val r = if null Ps then Extraction.nullt
   14.53 -          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
   14.54 -            (if dummy then
   14.55 -               [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
   14.56 -             else []) @
   14.57 -            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   14.58 -            [Bound (length prems)]));
   14.59 +        val r =
   14.60 +          if null Ps then Extraction.nullt
   14.61 +          else
   14.62 +            fold_rev (Term.abs o pair "x") Ts
   14.63 +              (list_comb (Const (case_name, T),
   14.64 +                (if dummy then
   14.65 +                   [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
   14.66 +                 else []) @
   14.67 +                map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   14.68 +                [Bound (length prems)]));
   14.69          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   14.70          val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
   14.71          val rews = map mk_meta_eq case_thms;
    15.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Jan 14 20:05:58 2012 +0100
    15.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 14 21:16:15 2012 +0100
    15.3 @@ -101,7 +101,7 @@
    15.4              NONE => NONE
    15.5            | SOME (bop, (m, p, S, S')) =>
    15.6                SOME (close (Goal.prove (Simplifier.the_context ss) [] [])
    15.7 -                (Logic.mk_equals (t, list_abs (xs, m $ p $ (bop $ S $ S'))))
    15.8 +                (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
    15.9                  (K (EVERY
   15.10                    [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
   15.11                     EVERY [etac conjE 1, rtac IntI 1, simp, simp,
   15.12 @@ -370,9 +370,9 @@
   15.13          val x' = map_type (K (HOLogic.mk_setT T)) x
   15.14        in
   15.15          (cterm_of thy x,
   15.16 -         cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
   15.17 -           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
   15.18 -      end) fs
   15.19 +         cterm_of thy (fold_rev (Term.abs o pair "x") Ts
   15.20 +          (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
   15.21 +      end) fs;
   15.22    in
   15.23      thm |>
   15.24      Thm.instantiate ([], insts) |>
   15.25 @@ -434,9 +434,9 @@
   15.26              (x, (x',
   15.27                (HOLogic.Collect_const T $
   15.28                   HOLogic.mk_psplits fs T HOLogic.boolT x',
   15.29 -               list_abs (map (pair "x") Ts, HOLogic.mk_mem
   15.30 -                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
   15.31 -                  x)))))
   15.32 +               fold_rev (Term.abs o pair "x") Ts
   15.33 +                 (HOLogic.mk_mem
   15.34 +                   (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
   15.35            end
   15.36         | NONE => (x, (x, (x, x))))) params;
   15.37      val (params1, (params2, params3)) =
   15.38 @@ -503,8 +503,8 @@
   15.39            Goal.prove lthy (map (fst o dest_Free) params) []
   15.40              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   15.41                (list_comb (p, params3),
   15.42 -               list_abs (map (pair "x") Ts, HOLogic.mk_mem
   15.43 -                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   15.44 +               fold_rev (Term.abs o pair "x") Ts
   15.45 +                (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   15.46                    list_comb (c, params))))))
   15.47              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   15.48                [def, mem_Collect_eq, @{thm split_conv}]) 1))
    16.1 --- a/src/HOL/Tools/record.ML	Sat Jan 14 20:05:58 2012 +0100
    16.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 14 21:16:15 2012 +0100
    16.3 @@ -1484,8 +1484,8 @@
    16.4                  NONE => error "try_param_tac: no such variable"
    16.5                | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
    16.6            | (_, T) :: _ =>
    16.7 -              [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
    16.8 -                (x, list_abs (params, Bound 0))])) rule';
    16.9 +              [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
   16.10 +                (x, fold_rev Term.abs params (Bound 0))])) rule';
   16.11    in compose_tac (false, rule'', nprems_of rule) i end);
   16.12  
   16.13  
    17.1 --- a/src/Provers/hypsubst.ML	Sat Jan 14 20:05:58 2012 +0100
    17.2 +++ b/src/Provers/hypsubst.ML	Sat Jan 14 21:16:15 2012 +0100
    17.3 @@ -156,18 +156,20 @@
    17.4          val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
    17.5            (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
    17.6          val (Ts, V) = split_last (Term.binder_types T);
    17.7 -        val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
    17.8 -            Bound j => subst_bounds (map Bound
    17.9 -              ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   17.10 -          | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   17.11 +        val u =
   17.12 +          fold_rev Term.abs (ps @ [("x", U)])
   17.13 +            (case (if b then t else t') of
   17.14 +              Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   17.15 +            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   17.16          val thy = Thm.theory_of_thm rl';
   17.17          val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
   17.18 -      in compose_tac (true, Drule.instantiate_normalize (instT,
   17.19 -        map (pairself (cterm_of thy))
   17.20 -          [(Var (ixn, Ts ---> U --> body_type T), u),
   17.21 -           (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
   17.22 -           (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
   17.23 -        nprems_of rl) i
   17.24 +      in
   17.25 +        compose_tac (true, Drule.instantiate_normalize (instT,
   17.26 +          map (pairself (cterm_of thy))
   17.27 +            [(Var (ixn, Ts ---> U --> body_type T), u),
   17.28 +             (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   17.29 +             (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   17.30 +          nprems_of rl) i
   17.31        end
   17.32    | NONE => no_tac);
   17.33  
    18.1 --- a/src/Pure/Isar/auto_bind.ML	Sat Jan 14 20:05:58 2012 +0100
    18.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Jan 14 21:16:15 2012 +0100
    18.3 @@ -26,7 +26,7 @@
    18.4  fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
    18.5  
    18.6  fun statement_binds thy name prop =
    18.7 -  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
    18.8 +  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
    18.9  
   18.10  
   18.11  (* goal *)
   18.12 @@ -39,7 +39,7 @@
   18.13  
   18.14  fun get_arg thy prop =
   18.15    (case strip_judgment thy prop of
   18.16 -    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
   18.17 +    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
   18.18    | _ => NONE);
   18.19  
   18.20  fun facts _ [] = []
    19.1 --- a/src/Pure/Isar/obtain.ML	Sat Jan 14 20:05:58 2012 +0100
    19.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 21:16:15 2012 +0100
    19.3 @@ -286,7 +286,7 @@
    19.4          val ts = map Free ps;
    19.5          val asms =
    19.6            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
    19.7 -          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
    19.8 +          |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), []));
    19.9          val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
   19.10        in
   19.11          state'
    20.1 --- a/src/Pure/Isar/rule_cases.ML	Sat Jan 14 20:05:58 2012 +0100
    20.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 14 21:16:15 2012 +0100
    20.3 @@ -76,7 +76,6 @@
    20.4  
    20.5  local
    20.6  
    20.7 -fun abs xs t = Term.list_abs (xs, t);
    20.8  fun app us t = Term.betapplys (t, us);
    20.9  
   20.10  fun dest_binops cs tm =
   20.11 @@ -115,10 +114,12 @@
   20.12      fun extract prop =
   20.13        let
   20.14          val (fixes1, fixes2) = extract_fixes case_outline prop;
   20.15 -        val abs_fixes = abs (fixes1 @ fixes2);
   20.16 +        val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2);
   20.17          fun abs_fixes1 t =
   20.18            if not nested then abs_fixes t
   20.19 -          else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
   20.20 +          else
   20.21 +            fold_rev Term.abs fixes1
   20.22 +              (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
   20.23          val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
   20.24            |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   20.25  
    21.1 --- a/src/Pure/Proof/extraction.ML	Sat Jan 14 20:05:58 2012 +0100
    21.2 +++ b/src/Pure/Proof/extraction.ML	Sat Jan 14 21:16:15 2012 +0100
    21.3 @@ -283,11 +283,14 @@
    21.4      val {typeof_eqns, ...} = ExtractionData.get thy;
    21.5      fun err () = error ("Unable to determine type of extracted program for\n" ^
    21.6        Syntax.string_of_term_global thy t)
    21.7 -  in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
    21.8 -    [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
    21.9 -      Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   21.10 +  in
   21.11 +    (case
   21.12 +      strip_abs_body
   21.13 +        (freeze_thaw (condrew thy (#net typeof_eqns) [typeof_proc [] vs])
   21.14 +          (fold (Term.abs o pair "x") Ts
   21.15 +            (Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   21.16        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
   21.17 -    | _ => err ()
   21.18 +    | _ => err ())
   21.19    end;
   21.20  
   21.21  (** realizers for axioms / theorems, together with correctness proofs **)
   21.22 @@ -513,9 +516,10 @@
   21.23      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   21.24      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
   21.25  
   21.26 -    fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
   21.27 -      (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   21.28 -        (map (pair "x") (rev Ts), t)));
   21.29 +    fun app_rlz_rews Ts vs t =
   21.30 +      strip_abs (length Ts)
   21.31 +        (freeze_thaw (condrew thy' rrews (procs @ [typroc vs, rlz_proc]))
   21.32 +          (fold (Term.abs o pair "x") Ts t));
   21.33  
   21.34      fun realizes_null vs prop = app_rlz_rews [] vs
   21.35        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
   21.36 @@ -564,7 +568,7 @@
   21.37                  val u' = (case AList.lookup (op =) types (tname_of T) of
   21.38                      SOME ((_, SOME f)) => f r eT u T
   21.39                    | _ => Const ("realizes", eT --> T --> T) $ r $ u)
   21.40 -              in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
   21.41 +              in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
   21.42            in (defs', corr_prf % SOME u) end
   21.43  
   21.44        | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
    22.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Jan 14 20:05:58 2012 +0100
    22.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Jan 14 21:16:15 2012 +0100
    22.3 @@ -284,8 +284,8 @@
    22.4        | hidden_variable (Free f) = not (member (op =) tf f)
    22.5        | hidden_variable _ = false;
    22.6  
    22.7 -    fun mk_default' T = list_abs
    22.8 -      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
    22.9 +    fun mk_default' T =
   22.10 +      fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
   22.11  
   22.12      fun elim_varst (t $ u) = elim_varst t $ elim_varst u
   22.13        | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
    23.1 --- a/src/Pure/pattern.ML	Sat Jan 14 20:05:58 2012 +0100
    23.2 +++ b/src/Pure/pattern.ML	Sat Jan 14 21:16:15 2012 +0100
    23.3 @@ -281,16 +281,18 @@
    23.4  
    23.5  (* put a term into eta long beta normal form *)
    23.6  fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
    23.7 -  | eta_long Ts t = (case strip_comb t of
    23.8 -      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
    23.9 -    | (u, ts) =>
   23.10 -      let
   23.11 -        val Us = binder_types (fastype_of1 (Ts, t));
   23.12 -        val i = length Us
   23.13 -      in list_abs (map (pair "x") Us,
   23.14 -        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
   23.15 -          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
   23.16 -      end);
   23.17 +  | eta_long Ts t =
   23.18 +      (case strip_comb t of
   23.19 +        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
   23.20 +      | (u, ts) =>
   23.21 +          let
   23.22 +            val Us = binder_types (fastype_of1 (Ts, t));
   23.23 +            val i = length Us;
   23.24 +          in
   23.25 +            fold_rev (Term.abs o pair "x") Us
   23.26 +              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
   23.27 +                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
   23.28 +          end);
   23.29  
   23.30  
   23.31  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
    24.1 --- a/src/Pure/term.ML	Sat Jan 14 20:05:58 2012 +0100
    24.2 +++ b/src/Pure/term.ML	Sat Jan 14 21:16:15 2012 +0100
    24.3 @@ -56,7 +56,6 @@
    24.4    val type_of: term -> typ
    24.5    val fastype_of1: typ list * term -> typ
    24.6    val fastype_of: term -> typ
    24.7 -  val list_abs: (string * typ) list * term -> term
    24.8    val strip_abs: term -> (string * typ) list * term
    24.9    val strip_abs_body: term -> term
   24.10    val strip_abs_vars: term -> (string * typ) list
   24.11 @@ -121,6 +120,7 @@
   24.12    val itselfT: typ -> typ
   24.13    val a_itselfT: typ
   24.14    val argument_type_of: term -> int -> typ
   24.15 +  val abs: string * typ -> term -> term
   24.16    val add_tvar_namesT: typ -> indexname list -> indexname list
   24.17    val add_tvar_names: term -> indexname list -> indexname list
   24.18    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   24.19 @@ -353,7 +353,7 @@
   24.20    in arg k [] tm end;
   24.21  
   24.22  
   24.23 -val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
   24.24 +fun abs (x, T) t = Abs (x, T, t);
   24.25  
   24.26  fun strip_abs (Abs (a, T, t)) =
   24.27        let val (a', t') = strip_abs t
    25.1 --- a/src/Pure/unify.ML	Sat Jan 14 20:05:58 2012 +0100
    25.2 +++ b/src/Pure/unify.ML	Sat Jan 14 21:16:15 2012 +0100
    25.3 @@ -339,7 +339,7 @@
    25.4        in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end;
    25.5  
    25.6  
    25.7 -(*Abstraction over a list of types, like list_abs*)
    25.8 +(*Abstraction over a list of types*)
    25.9  fun types_abs ([], u) = u
   25.10    | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
   25.11  
    26.1 --- a/src/Tools/cong_tac.ML	Sat Jan 14 20:05:58 2012 +0100
    26.2 +++ b/src/Tools/cong_tac.ML	Sat Jan 14 21:16:15 2012 +0100
    26.3 @@ -25,7 +25,7 @@
    26.4              Logic.strip_assums_concl (Thm.prop_of cong');
    26.5            val ps = Logic.strip_params (Thm.concl_of cong');
    26.6            val insts = [(f', f), (g', g), (x', x), (y', y)]
    26.7 -            |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
    26.8 +            |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
    26.9          in
   26.10            fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
   26.11              handle THM _ => no_tac st