# HG changeset patch
# User wenzelm
# Date 1326572175 -3600
# Node ID 426ed18eba433c6a1409481cfcfc3d12c02e6c08
# Parent  ecf6375e2abb3d0301b6c2a0ca72c158d3ff963f
discontinued old-style Term.list_abs in favour of plain Term.abs;

diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -231,12 +231,13 @@
             let val T = type_of x
             in if Datatype_Aux.is_rec_type dt then
                 let val Us = binder_types T
-                in list_abs (map (pair "x") Us,
-                  Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
-                    list_comb (x, map (fn (i, U) =>
-                      Const ("Nominal.perm", permT --> U --> U) $
-                        (Const ("List.rev", permT --> permT) $ pi) $
-                        Bound i) ((length Us - 1 downto 0) ~~ Us)))
+                in
+                  fold_rev (Term.abs o pair "x") Us
+                    (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
+                      list_comb (x, map (fn (i, U) =>
+                        Const ("Nominal.perm", permT --> U --> U) $
+                          (Const ("List.rev", permT --> permT) $ pi) $
+                          Bound i) ((length Us - 1 downto 0) ~~ Us)))
                 end
               else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
             end;
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -23,7 +23,7 @@
     val Ts = map snd ps;
     val tinst' = map (fn (t, u) =>
       (head_of (Logic.incr_indexes (Ts, j) t),
-       list_abs (ps, u))) tinst;
+       fold_rev Term.abs ps u)) tinst;
     val th' = instf
       (map (pairself (ctyp_of thy)) tyinst')
       (map (pairself (cterm_of thy)) tinst')
@@ -155,9 +155,10 @@
    let val vars' = Misc_Legacy.term_vars (prop_of st);
        val thy = theory_of_thm st;
    in case subtract (op =) vars vars' of
-     [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
+     [x] =>
+      Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
     | _ => error "fresh_fun_simp: Too many variables, please report."
-  end
+   end
   in
   ((fn st =>
   let
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -301,8 +301,8 @@
             val s = fold_rev (fn v => fn s =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
               vs HOLogic.unit;
-            val s' = list_abs (ps,
-              Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+            val s' = fold_rev Term.abs ps
+              (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
                 Term.range_type T) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
@@ -345,8 +345,9 @@
             val s = fold_rev (fn v => fn s =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
               vs HOLogic.unit;
-            val s' = list_abs (ps,
-              Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
+            val s' =
+              fold_rev Term.abs ps
+                (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -381,8 +381,8 @@
               (Logic.mk_implies
                 (HOLogic.mk_Trueprop (HOLogic.list_all
                    (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
-                 HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
-                   r $ (a $ Datatype_Aux.app_bnds f i)), f))))
+                 HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
+                   (r $ (a $ Datatype_Aux.app_bnds f i)), f))))
               (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
                  REPEAT (etac allE 1), rtac thm 1, atac 1])
           end
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -345,7 +345,7 @@
             val (xs, ys) =
               if j < i then (zs @ map (pair "x") (drop j Us), [])
               else chop i zs;
-            val u = list_abs (ys, strip_abs_body t);
+            val u = fold_rev Term.abs ys (strip_abs_body t);
             val xs' = map Free
               ((fold_map Name.variant (map fst xs)
                   (Term.declare_term_names u used) |> fst) ~~
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -235,8 +235,8 @@
 
         fun mk_reccomb ((dt, T), t) =
           let val (Us, U) = strip_type T in
-            list_abs (map (pair "x") Us,
-              nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
+            fold_rev (Term.abs o pair "x") Us
+              (nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
           end;
 
         val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees');
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -216,8 +216,8 @@
         (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
-        list_abs (map dest_Free rs, list_comb (r,
-          map Bound ((length rs - 1 downto 0) @ [length rs])))));
+        (fold_rev (Term.abs o dest_Free) rs
+          (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
   in
     Extraction.add_realizers_i
       [(exh_name, (["P"], r', prf)),
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -2119,9 +2119,8 @@
 fun ap_curry [_] _ t = t
   | ap_curry arg_Ts tuple_T t =
     let val n = length arg_Ts in
-      list_abs (map (pair "c") arg_Ts,
-                incr_boundvars n t
-                $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
+      fold_rev (Term.abs o pair "c") arg_Ts
+                (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
     end
 
 fun num_occs_of_bound_in_term j (t1 $ t2) =
@@ -2182,9 +2181,9 @@
           val step_body = recs |> map (repair_rec j)
                                |> List.foldl s_disj @{const False}
         in
-          (list_abs (tl xs, incr_bv (~1, j, base_body))
+          (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
            |> ap_n_split (length arg_Ts) tuple_T bool_T,
-           Abs ("y", tuple_T, list_abs (tl xs, step_body)
+           Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
                               |> ap_n_split (length arg_Ts) tuple_T bool_T))
         end
       | aux t =
@@ -2235,7 +2234,7 @@
       image_const $ (rtrancl_const $ step_set) $ base_set
       |> predicatify tuple_T
   in
-    list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
+    fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T)
     |> unfold_defs_in_term hol_ctxt
   end
 
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -436,7 +436,7 @@
     val bs = map (pair "x") inpTs
     val bounds = map Bound (rev (0 upto (length bs) - 1))
     val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
-  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
+  in fold_rev Term.abs bs (mk_single compfuns (list_comb (f, bounds))) end
 
 fun register_alternative_function pred_name mode fun_name =
   Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -703,12 +703,12 @@
         let
           val bs = map (pair "x") (binder_types (fastype_of t))
           val bounds = map Bound (rev (0 upto (length bs) - 1))
-        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
+        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
       | (t, Context m) =>
         let
           val bs = map (pair "x") (binder_types (fastype_of t))
           val bounds = map Bound (rev (0 upto (length bs) - 1))
-        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
+        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
       | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
         (case (expr_of (t1, d1), expr_of (t2, d2)) of
           (NONE, NONE) => NONE
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -235,10 +235,10 @@
                             Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
                           val Ts = binder_types (fastype_of t)
                         in
-                          list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
-                            mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
-                            HOLogic.mk_eq (@{term True}, Bound 0),
-                            HOLogic.mk_eq (@{term False}, Bound 0)))
+                          fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})])
+                            (mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
+                              HOLogic.mk_eq (@{term True}, Bound 0),
+                              HOLogic.mk_eq (@{term False}, Bound 0)))
                         end
                     val argvs' = map2 lift_arg Ts argvs
                     val resname = singleton (Name.variant_list names') "res"
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -462,7 +462,7 @@
       let
         val frees = Term.add_frees t []
         val t' = fold_rev absfree frees t
-        fun wrap f t = list_abs (f (strip_abs t))
+        fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -652,9 +652,10 @@
                 val k = length Ts;
                 val bs = map Bound (k - 1 downto 0);
                 val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
-                val Q = list_abs (mk_names "x" k ~~ Ts,
-                  HOLogic.mk_binop inductive_conj_name
-                    (list_comb (incr_boundvars k s, bs), P));
+                val Q =
+                  fold_rev Term.abs (mk_names "x" k ~~ Ts)
+                    (HOLogic.mk_binop inductive_conj_name
+                      (list_comb (incr_boundvars k s, bs), P));
               in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
           | NONE =>
               (case s of
@@ -760,9 +761,10 @@
             val l = length Us;
             val zs = map Bound (l - 1 downto 0);
           in
-            list_abs (map (pair "z") Us, list_comb (p,
-              make_bool_args' bs i @ make_args argTs
-                ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
+            fold_rev (Term.abs o pair "z") Us
+              (list_comb (p,
+                make_bool_args' bs i @ make_args argTs
+                  ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
           end
       | NONE =>
           (case t of
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -88,8 +88,9 @@
           val u = list_comb (t, map Bound (i - 1 downto 0))
         in 
           if member (op =) vs a then
-            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
-          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
+            fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
+          else
+            fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
         end
   | gen_rvar _ t = t;
 
@@ -164,24 +165,25 @@
                 let
                   val prem' :: prems' = prems;
                   val U = Extraction.etype_of thy vs [] prem';
-                in if U = Extraction.nullT
+                in
+                  if U = Extraction.nullT
                   then fun_of (Free (x, T) :: ts)
                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
                     (Free (x, T) :: args) (x :: r :: used) prems'
                   else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
                     (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
                 end
-              else (case strip_type T of
+              else
+                (case strip_type T of
                   (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
                     let
                       val fx = Free (x, Ts ---> T1);
                       val fr = Free (r, Ts ---> T2);
                       val bs = map Bound (length Ts - 1 downto 0);
-                      val t = list_abs (map (pair "z") Ts,
-                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
-                    in fun_of (fx :: ts) (fr :: rts) (t::args)
-                      (x :: r :: used) prems
-                    end
+                      val t =
+                        fold_rev (Term.abs o pair "z") Ts
+                          (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
+                    in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
                 | (Ts, U) => fun_of (Free (x, T) :: ts)
                     (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
                     (Free (x, T) :: args) (x :: r :: used) prems)
@@ -439,13 +441,16 @@
         val T' = Extraction.etype_of thy (vs @ Ps) [] p;
         val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
         val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
-        val r = if null Ps then Extraction.nullt
-          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
-            (if dummy then
-               [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
-             else []) @
-            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
-            [Bound (length prems)]));
+        val r =
+          if null Ps then Extraction.nullt
+          else
+            fold_rev (Term.abs o pair "x") Ts
+              (list_comb (Const (case_name, T),
+                (if dummy then
+                   [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
+                 else []) @
+                map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
+                [Bound (length prems)]));
         val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
         val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
         val rews = map mk_meta_eq case_thms;
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -101,7 +101,7 @@
             NONE => NONE
           | SOME (bop, (m, p, S, S')) =>
               SOME (close (Goal.prove (Simplifier.the_context ss) [] [])
-                (Logic.mk_equals (t, list_abs (xs, m $ p $ (bop $ S $ S'))))
+                (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
                 (K (EVERY
                   [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
                    EVERY [etac conjE 1, rtac IntI 1, simp, simp,
@@ -370,9 +370,9 @@
         val x' = map_type (K (HOLogic.mk_setT T)) x
       in
         (cterm_of thy x,
-         cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
-           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
-      end) fs
+         cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+          (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
+      end) fs;
   in
     thm |>
     Thm.instantiate ([], insts) |>
@@ -434,9 +434,9 @@
             (x, (x',
               (HOLogic.Collect_const T $
                  HOLogic.mk_psplits fs T HOLogic.boolT x',
-               list_abs (map (pair "x") Ts, HOLogic.mk_mem
-                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
-                  x)))))
+               fold_rev (Term.abs o pair "x") Ts
+                 (HOLogic.mk_mem
+                   (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
           end
        | NONE => (x, (x, (x, x))))) params;
     val (params1, (params2, params3)) =
@@ -503,8 +503,8 @@
           Goal.prove lthy (map (fst o dest_Free) params) []
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
               (list_comb (p, params3),
-               list_abs (map (pair "x") Ts, HOLogic.mk_mem
-                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
+               fold_rev (Term.abs o pair "x") Ts
+                (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, @{thm split_conv}]) 1))
diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/record.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -1484,8 +1484,8 @@
                 NONE => error "try_param_tac: no such variable"
               | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
           | (_, T) :: _ =>
-              [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
-                (x, list_abs (params, Bound 0))])) rule';
+              [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
+                (x, fold_rev Term.abs params (Bound 0))])) rule';
   in compose_tac (false, rule'', nprems_of rule) i end);
 
 
diff -r ecf6375e2abb -r 426ed18eba43 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Provers/hypsubst.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -156,18 +156,20 @@
         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
         val (Ts, V) = split_last (Term.binder_types T);
-        val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
-            Bound j => subst_bounds (map Bound
-              ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
-          | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
+        val u =
+          fold_rev Term.abs (ps @ [("x", U)])
+            (case (if b then t else t') of
+              Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
+            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
         val thy = Thm.theory_of_thm rl';
         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
-      in compose_tac (true, Drule.instantiate_normalize (instT,
-        map (pairself (cterm_of thy))
-          [(Var (ixn, Ts ---> U --> body_type T), u),
-           (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
-           (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
-        nprems_of rl) i
+      in
+        compose_tac (true, Drule.instantiate_normalize (instT,
+          map (pairself (cterm_of thy))
+            [(Var (ixn, Ts ---> U --> body_type T), u),
+             (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
+             (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
+          nprems_of rl) i
       end
   | NONE => no_tac);
 
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -26,7 +26,7 @@
 fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
 
 fun statement_binds thy name prop =
-  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
+  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
 
 
 (* goal *)
@@ -39,7 +39,7 @@
 
 fun get_arg thy prop =
   (case strip_judgment thy prop of
-    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
+    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
   | _ => NONE);
 
 fun facts _ [] = []
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -286,7 +286,7 @@
         val ts = map Free ps;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
-          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
+          |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), []));
         val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
       in
         state'
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -76,7 +76,6 @@
 
 local
 
-fun abs xs t = Term.list_abs (xs, t);
 fun app us t = Term.betapplys (t, us);
 
 fun dest_binops cs tm =
@@ -115,10 +114,12 @@
     fun extract prop =
       let
         val (fixes1, fixes2) = extract_fixes case_outline prop;
-        val abs_fixes = abs (fixes1 @ fixes2);
+        val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2);
         fun abs_fixes1 t =
           if not nested then abs_fixes t
-          else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
+          else
+            fold_rev Term.abs fixes1
+              (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
         val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
 
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -283,11 +283,14 @@
     val {typeof_eqns, ...} = ExtractionData.get thy;
     fun err () = error ("Unable to determine type of extracted program for\n" ^
       Syntax.string_of_term_global thy t)
-  in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
-    [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
-      Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
+  in
+    (case
+      strip_abs_body
+        (freeze_thaw (condrew thy (#net typeof_eqns) [typeof_proc [] vs])
+          (fold (Term.abs o pair "x") Ts
+            (Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
       Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
-    | _ => err ()
+    | _ => err ())
   end;
 
 (** realizers for axioms / theorems, together with correctness proofs **)
@@ -513,9 +516,10 @@
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
     fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
 
-    fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
-      (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
-        (map (pair "x") (rev Ts), t)));
+    fun app_rlz_rews Ts vs t =
+      strip_abs (length Ts)
+        (freeze_thaw (condrew thy' rrews (procs @ [typroc vs, rlz_proc]))
+          (fold (Term.abs o pair "x") Ts t));
 
     fun realizes_null vs prop = app_rlz_rews [] vs
       (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
@@ -564,7 +568,7 @@
                 val u' = (case AList.lookup (op =) types (tname_of T) of
                     SOME ((_, SOME f)) => f r eT u T
                   | _ => Const ("realizes", eT --> T --> T) $ r $ u)
-              in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
+              in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
           in (defs', corr_prf % SOME u) end
 
       | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -284,8 +284,8 @@
       | hidden_variable (Free f) = not (member (op =) tf f)
       | hidden_variable _ = false;
 
-    fun mk_default' T = list_abs
-      (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
+    fun mk_default' T =
+      fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
 
     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/pattern.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -281,16 +281,18 @@
 
 (* put a term into eta long beta normal form *)
 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
-  | eta_long Ts t = (case strip_comb t of
-      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-    | (u, ts) =>
-      let
-        val Us = binder_types (fastype_of1 (Ts, t));
-        val i = length Us
-      in list_abs (map (pair "x") Us,
-        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
-      end);
+  | eta_long Ts t =
+      (case strip_comb t of
+        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
+      | (u, ts) =>
+          let
+            val Us = binder_types (fastype_of1 (Ts, t));
+            val i = length Us;
+          in
+            fold_rev (Term.abs o pair "x") Us
+              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+          end);
 
 
 (*Tests whether 2 terms are alpha/eta-convertible and have same type.
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/term.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -56,7 +56,6 @@
   val type_of: term -> typ
   val fastype_of1: typ list * term -> typ
   val fastype_of: term -> typ
-  val list_abs: (string * typ) list * term -> term
   val strip_abs: term -> (string * typ) list * term
   val strip_abs_body: term -> term
   val strip_abs_vars: term -> (string * typ) list
@@ -121,6 +120,7 @@
   val itselfT: typ -> typ
   val a_itselfT: typ
   val argument_type_of: term -> int -> typ
+  val abs: string * typ -> term -> term
   val add_tvar_namesT: typ -> indexname list -> indexname list
   val add_tvar_names: term -> indexname list -> indexname list
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
@@ -353,7 +353,7 @@
   in arg k [] tm end;
 
 
-val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
+fun abs (x, T) t = Abs (x, T, t);
 
 fun strip_abs (Abs (a, T, t)) =
       let val (a', t') = strip_abs t
diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/unify.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -339,7 +339,7 @@
       in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end;
 
 
-(*Abstraction over a list of types, like list_abs*)
+(*Abstraction over a list of types*)
 fun types_abs ([], u) = u
   | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
 
diff -r ecf6375e2abb -r 426ed18eba43 src/Tools/cong_tac.ML
--- a/src/Tools/cong_tac.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Tools/cong_tac.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -25,7 +25,7 @@
             Logic.strip_assums_concl (Thm.prop_of cong');
           val ps = Logic.strip_params (Thm.concl_of cong');
           val insts = [(f', f), (g', g), (x', x), (y', y)]
-            |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
+            |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
         in
           fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
             handle THM _ => no_tac st