# HG changeset patch
# User wenzelm
# Date 1313597131 -7200
# Node ID 7943b69f0188b99760921090b9a09ca98fbb1802
# Parent  4b1a63678839e31473e2927ff9ca8684d2810b6a
modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;

diff -r 4b1a63678839 -r 7943b69f0188 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/CCL/Term.thy	Wed Aug 17 18:05:31 2011 +0200
@@ -58,18 +58,18 @@
 (* FIXME does not handle "_idtdummy" *)
 (* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
 
-fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
+fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
 fun let_tr' [a,Abs(id,T,b)] =
      let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
      in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
 
-fun letrec_tr [Free(f,S),Free(x,T),a,b] =
-      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
-fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
-      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
-fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
-      Const(@{const_syntax letrec3},dummyT) $
-        absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
+fun letrec_tr [Free f, Free x, a, b] =
+      Const(@{const_syntax letrec}, dummyT) $ absfree x (absfree f a) $ absfree f b;
+fun letrec2_tr [Free f, Free x, Free y, a, b] =
+      Const(@{const_syntax letrec2}, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
+fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
+      Const(@{const_syntax letrec3}, dummyT) $
+        absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
 
 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
      let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
diff -r 4b1a63678839 -r 7943b69f0188 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/FOL/fologic.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -76,10 +76,10 @@
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
-fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
+fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
 
 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
-fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
 
 
 (* binary oprations and relations *)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -393,7 +393,7 @@
     quant "forall" HOLogic.all_const ||
     quant "exists" HOLogic.exists_const ||
     scan_fail "illegal quantifier kind"
-  fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
+  fun mk_quant q (x, T) t = q T $ absfree (x, T) t
 
   val patternT = @{typ "SMT.pattern"}
   fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -54,7 +54,7 @@
 (* building terms *)
 
 fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT)
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P)
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
 
 fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT)
 
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Hoare/Separation.thy	Wed Aug 17 18:05:31 2011 +0200
@@ -68,11 +68,11 @@
 fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
   | singl_tr ts = raise TERM ("singl_tr", ts);
 fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
-      absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
+      absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $
       Syntax.free "H"
   | star_tr ts = raise TERM ("star_tr", ts);
 fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
-      absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
+      absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H"
   | wand_tr ts = raise TERM ("wand_tr", ts);
 *}
 
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -28,17 +28,21 @@
 
 (** abstraction of body over a tuple formed from a list of free variables.
 Types are also built **)
-fun mk_abstupleC []     body = absfree ("x", HOLogic.unitT, body)
-  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
-                               in if w=[] then absfree (n, T, body)
-        else let val z  = mk_abstupleC w body;
-                 val T2 = case z of Abs(_,T,_) => T
-                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
-       in
+fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
+  | mk_abstupleC [v] body = absfree (dest_Free v) body
+  | mk_abstupleC (v :: w) body =
+      let
+        val (x, T) = dest_Free v;
+        val z = mk_abstupleC w body;
+        val T2 =
+          (case z of
+            Abs (_, T, _) => T
+          | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
+      in
         Const (@{const_name prod_case},
-          (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT)
-            $ absfree (n, T, z)
-       end end;
+            (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
+          absfree (x, T) z
+      end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
 fun mk_bodyC []      = HOLogic.unit
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 17 18:05:31 2011 +0200
@@ -102,16 +102,16 @@
     let
       val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
     in
-      absdummy (@{typ nat}, absdummy (@{typ nat},
-        Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
+      absdummy @{typ nat} (absdummy @{typ nat}
+        (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
           (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
           Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
           Predicate_Compile_Aux.mk_single compfuns
           (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
     end
   fun enumerate_addups_nat compfuns (_ : typ) =
-    absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
-    (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
+    absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
+    (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $
       (@{term "Code_Numeral.nat_of"} $ Bound 0) $
       (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
       @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
@@ -120,8 +120,8 @@
       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
       val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
     in
-      absdummy(@{typ nat}, absdummy (@{typ nat},
-        Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
+      absdummy @{typ nat} (absdummy @{typ nat}
+        (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
           (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
             @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -1678,7 +1678,7 @@
               fresh_fs @
           map (fn (((P, T), (x, U)), Q) =>
            (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
-            Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
+            Abs ("z", HOLogic.unitT, absfree (x, U) Q)))
               (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
           map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
             rec_unique_frees)) induct_aux;
@@ -2017,9 +2017,9 @@
           (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
-          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
-           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
-             set $ Free ("x", T) $ Free ("y", T'))))))
+          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T)
+           (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
+             (set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
 
     (* prove characteristic equations for primrec combinators *)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -187,7 +187,7 @@
         fun mk s =
           let
             val t = Syntax.read_term ctxt' s;
-            val t' = list_abs_free (params, t) |>
+            val t' = fold_rev absfree params t |>
               funpow (length params) (fn Abs (_, _, t) => t)
           in (t', HOLogic.dest_setT (fastype_of t)) end
           handle TERM _ =>
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -163,8 +163,7 @@
               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
                 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
                   handle RecError s => primrec_eq_err lthy s eq
-            in (fnames'', fnss'',
-                (list_abs_free (cargs' @ subs, rhs'))::fns)
+            in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns)
             end)
 
   in (case AList.lookup (op =) fnames i of
@@ -209,8 +208,8 @@
     val used = map fst (fold Term.add_frees fs []);
     val x = (singleton (Name.variant_list used) "x", dummyT);
     val frees = ls @ x :: rs;
-    val raw_rhs = list_abs_free (frees,
-      list_comb (Const (rec_name, dummyT), fs @ [Free x]))
+    val raw_rhs = fold_rev absfree frees
+      (list_comb (Const (rec_name, dummyT), fs @ [Free x]))
     val def_name = Thm.def_name (Long_Name.base_name fname);
     val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     val SOME var = get_first (fn ((b, _), mx) =>
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Set.thy	Wed Aug 17 18:05:31 2011 +0200
@@ -281,7 +281,7 @@
         val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
         val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
         val exP = ex_tr [idts, P];
-      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
+      in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
 
   in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
 *}
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -323,7 +323,7 @@
         val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
         val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
         val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
-        val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
+        val f = fold_rev (absfree o dest_Free) (xs @ ys) (mk_univ_inj ts n i);
 
         val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -201,10 +201,10 @@
       let
         val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
           Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
-            absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
+            absfree ("y", T2) (set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
               (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
         val cert = cterm_of thy1
-        val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
+        val insts = map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
           ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
@@ -238,9 +238,9 @@
       |> (Global_Theory.add_defs false o map Thm.no_attributes)
           (map (fn ((((name, comb), set), T), T') =>
             (Binding.name (Long_Name.base_name name ^ "_def"),
-              Logic.mk_equals (comb, absfree ("x", T,
-               Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
-                 set $ Free ("x", T) $ Free ("y", T'))))))
+              Logic.mk_equals (comb, absfree ("x", T)
+               (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
+                 (set $ Free ("x", T) $ Free ("y", T'))))))
                    (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
       ||> Sign.parent_path
       ||> Theory.checkpoint;
@@ -306,8 +306,7 @@
               val frees = take (length cargs) frees';
               val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
             in
-             (free, list_abs_free (map dest_Free frees',
-               list_comb (free, frees)))
+              (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
             end) (constrs ~~ (1 upto length constrs)));
 
           val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -145,7 +145,7 @@
       (case t1 of
         NONE =>
           (case flt (Misc_Legacy.term_frees t2) of
-            [Free (s, T)] => SOME (absfree (s, T, t2))
+            [Free (s, T)] => SOME (absfree (s, T) t2)
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
     val insts = map_filter (fn (t, u) =>
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -56,9 +56,8 @@
                   val rT = nth (rec_result_Ts) i;
                   val vs' = filter_out is_unit vs;
                   val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
-                  val f' = Envir.eta_contract (list_abs_free
-                    (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
-                      else HOLogic.unit));
+                  val f' = Envir.eta_contract (fold_rev (absfree o dest_Free) vs
+                    (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
                 in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
                   (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
                 end
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -68,8 +68,8 @@
           val args = Misc_Legacy.term_frees body
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
-            list_abs_free (map dest_Free args,
-                           HOLogic.choice_const T $ beta_eta_in_abs_body body)
+            fold_rev (absfree o dest_Free) args
+              (HOLogic.choice_const T $ beta_eta_in_abs_body body)
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -491,7 +491,7 @@
       case strip_comb flex of
         (Var (z as (_, T)), args) =>
         add_terms (Var z,
-          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
+          fold_rev absdummy (take (length args) (binder_types T)) rigid)
       | _ => I
     fun unify_potential_flex comb atom =
       if is_flex comb then unify_flex comb atom
@@ -541,7 +541,7 @@
            if k > j then t else t $ u
          | (t, u) => t $ u)
       | repair t = t
-    val t' = t |> repair |> fold (curry absdummy) (map snd params)
+    val t' = t |> repair |> fold (absdummy o snd) params
     fun do_instantiate th =
       case Term.add_vars (prop_of th) []
            |> filter_out ((Meson_Clausify.is_zapped_var_name orf
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -1555,7 +1555,7 @@
     else
       fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
   end
-  |> curry absdummy dataT
+  |> absdummy dataT
 
 fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
   let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
@@ -1968,7 +1968,7 @@
           discriminate_value hol_ctxt x y_var ::
           map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
           |> foldr1 s_conj
-      in List.foldr absdummy core_t arg_Ts end
+      in fold_rev absdummy arg_Ts core_t end
   in
     [HOLogic.mk_imp
        (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -634,7 +634,7 @@
                   fun app f =
                     list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
                 in
-                  List.foldr absdummy (connective $ app pos $ app neg) arg_Ts
+                  fold_rev absdummy arg_Ts (connective $ app pos $ app neg)
                 end
             end
           else
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -1017,7 +1017,7 @@
 
 fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
-    val t' = list_abs_free (Term.add_frees t [], t)
+    val t' = fold_rev absfree (Term.add_frees t []) t
     val options = code_options_of (Proof_Context.theory_of ctxt)
     val thy = Theory.copy (Proof_Context.theory_of ctxt)
     val ((((full_constname, constT), vs'), intro), thy1) =
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -914,7 +914,7 @@
             val Ts = binder_types (fastype_of f')
             val bs = map Bound ((length Ts - 1) downto 0)
           in
-            fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
+            fold_rev absdummy Ts (f $ (list_comb (f', bs)))
           end
         val fs' = map apply_f fs
         val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
@@ -949,7 +949,7 @@
       val T' = TFree (tname', HOLogic.typeS)
       val U = TFree (uname, HOLogic.typeS)
       val y = Free (yname, U)
-      val f' = absdummy (U --> T', Bound 0 $ y)
+      val f' = absdummy (U --> T') (Bound 0 $ y)
       val th' = Thm.certify_instantiate
         ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
          [((fst (dest_Var f), (U --> T') --> T'), f')]) th
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -524,7 +524,7 @@
          Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
          @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) 
       in
-        absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3)
+        absdummy @{typ code_numeral} (small_lazy $ HOLogic.mk_number @{typ int} 3)
       end
     ),
   modify_funT = I,
@@ -580,27 +580,29 @@
 
 (** specific rpred functions -- move them to the correct place in this file *)
 fun mk_Eval_of (P as (Free (f, _)), T) mode =
-let
-  fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
-    let
-      val (bs2, i') = mk_bounds T2 i 
-      val (bs1, i'') = mk_bounds T1 i'
-    in
-      (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
-    end
-    | mk_bounds T i = (Bound i, i + 1)
-  fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
-  fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
-    | mk_tuple tTs = foldr1 mk_prod tTs;
-  fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t = absdummy (T, HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
-    | mk_split_abs T t = absdummy (T, t)
-  val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
-  val (inargs, outargs) = split_mode mode args
-  val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
-  val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
-in
-  fold_rev mk_split_abs (binder_types T) inner_term  
-end
+  let
+    fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
+          let
+            val (bs2, i') = mk_bounds T2 i 
+            val (bs1, i'') = mk_bounds T1 i'
+          in
+            (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
+          end
+      | mk_bounds T i = (Bound i, i + 1)
+    fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
+    fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
+      | mk_tuple tTs = foldr1 mk_prod tTs
+    fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
+          absdummy T
+            (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
+      | mk_split_abs T t = absdummy T t
+    val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
+    val (inargs, outargs) = split_mode mode args
+    val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
+    val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
+  in
+    fold_rev mk_split_abs (binder_types T) inner_term
+  end
 
 fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
   let
@@ -1831,7 +1833,7 @@
     val t' =
       if stats andalso compilation = New_Pos_Random_DSeq then
         mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
-          (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
+          (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
             @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
       else
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -218,7 +218,7 @@
 
 fun compile_term compilation options ctxt t =
   let
-    val t' = list_abs_free (Term.add_frees t [], t)
+    val t' = fold_rev absfree (Term.add_frees t []) t
     val thy = Theory.copy (Proof_Context.theory_of ctxt)
     val ((((full_constname, constT), vs'), intro), thy1) =
       Predicate_Compile_Aux.define_quickcheck_predicate t' thy
@@ -269,7 +269,7 @@
         | Pos_Generator_DSeq => mk_gen_bind (prog,
             mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
             (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
-        | Depth_Limited_Random => fold_rev (curry absdummy)
+        | Depth_Limited_Random => fold_rev absdummy
             [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
              @{typ "code_numeral * code_numeral"}]
             (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -70,7 +70,7 @@
   end
 
 fun mk_unit_let (x, y) =
-  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
+  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
   
 (* handling inductive datatypes *)
 
@@ -113,14 +113,14 @@
     map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   end
 
-fun gen_mk_call c T =  (T, fn t => c T $ absdummy (T, t) $ size_pred)
+fun gen_mk_call c T =  (T, fn t => c T $ absdummy T t $ size_pred)
 
 fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
   let
     val T = Type (tyco, Ts)
     val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   in
-   (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
+   (T, fn t => nth functerms k $ absdummy T t $ size_pred)
   end
 
 fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
@@ -184,18 +184,18 @@
           Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
             full_exhaustiveT T)
       in
-        (T, (fn t => full_exhaustive $
+        (T, fn t => full_exhaustive $
           (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
-          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
+          $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
       end
     fun mk_aux_call fTs (k, _) (tyco, Ts) =
       let
         val T = Type (tyco, Ts)
         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
       in
-        (T, (fn t => nth functerms k $
+        (T, fn t => nth functerms k $
           (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
-            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
+            $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
       end
     fun mk_consexpr simpleT (c, xs) =
       let
@@ -209,7 +209,7 @@
           bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
         val start_term = test_function simpleT $ 
         (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
-          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
+          $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
       in fold_rev (fn f => fn t => f t) fns start_term end
     fun mk_rhs exprs =
         @{term "If :: bool => term list option => term list option => term list option"}
@@ -382,7 +382,7 @@
 
 fun mk_parametric_generator_expr mk_generator_expr =
   Quickcheck_Common.gen_mk_parametric_generator_expr 
-    ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
+    ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: term list option"}),
       @{typ "code_numeral => term list option"})
 
 fun mk_validator_expr ctxt t =
@@ -412,9 +412,9 @@
     val return = @{term "Some :: term list => term list option"} $
       (HOLogic.mk_list @{typ "term"}
         (replicate (length frees + length eval_terms) dummy_term))
-    val wrap = absdummy (@{typ bool},
-      @{term "If :: bool => term list option => term list option => term list option"} $
-      Bound 0 $ @{term "None :: term list option"} $ return)
+    val wrap = absdummy @{typ bool}
+      (@{term "If :: bool => term list option => term list option => term list option"} $
+        Bound 0 $ @{term "None :: term list option"} $ return)
   in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   
 (** generator compiliation **)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -340,10 +340,11 @@
       in
         case dT of
           Type (@{type_name fun}, _) =>
-            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
-            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
-        | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
-            Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
+            (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+              Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
+        | _ =>
+            (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+              Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
       end
       | eval_function T = (I, T)
     val (tt, boundTs') = split_list (map eval_function boundTs)
@@ -432,7 +433,7 @@
       end
     else
       let
-        val t' = Term.list_abs_free (Term.add_frees t [], t)
+        val t' = fold_rev absfree (Term.add_frees t []) t
         fun wrap f t = list_abs (f (strip_abs t))
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -112,7 +112,7 @@
       if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
         (mk_generator_expr ctxt (t, eval_terms)) $ else_t
   in
-    absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
+    absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
   end
 
 (** post-processing of function terms **)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -291,7 +291,7 @@
 fun mk_generator_expr ctxt (t, eval_terms) =
   let  
     val thy = Proof_Context.theory_of ctxt
-    val prop = list_abs_free (Term.add_frees t [], t)
+    val prop = fold_rev absfree (Term.add_frees t []) t
     val Ts = (map snd o fst o strip_abs) prop
     val bound_max = length Ts - 1;
     val bounds = map_index (fn (i, ty) =>
@@ -317,7 +317,7 @@
 fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   let
     val thy = Proof_Context.theory_of ctxt
-    val prop = list_abs_free (Term.add_frees t [], t)
+    val prop = fold_rev absfree (Term.add_frees t []) t
     val Ts = (map snd o fst o strip_abs) prop
     val bound_max = length Ts - 1
     val bounds = map_index (fn (i, ty) =>
@@ -360,13 +360,13 @@
 
 val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_generator_expr, 
-    absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
+    absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => term list option * Random.seed"}),
     @{typ "code_numeral => Random.seed => term list option * Random.seed"})
 
 val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_reporting_generator_expr,
-    absdummy (@{typ code_numeral},
-      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
+    absdummy @{typ code_numeral}
+      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"}),
     @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
     
     
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -156,11 +156,11 @@
         val (dT', rT') = Term.dest_funT rT
       in
         mk_fun_upd dT rT $ f $ t $
-          mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
+          mk_update (ts, u) (absdummy dT' (Const ("_", rT')))
       end
 
 fun mk_lambda Ts (t, pats) =
-  fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
+  fold_rev absdummy Ts t |> fold mk_update pats
 
 fun translate ((t, k), (e, cs)) =
   let
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -145,7 +145,7 @@
     val frees = map Free (Term.add_frees t [])
     val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
     val vs = map (Term.dest_Free o Thm.term_of) cvs'
-  in (Term.list_abs_free (vs, t), cvs') end
+  in (fold_rev absfree vs t, cvs') end
 
 fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
   let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -342,8 +342,7 @@
  ("The following clauses are redundant (covered by preceding clauses): " ^
                    commas (map (fn i => string_of_int (i + 1)) L))
  in {functional = Abs(Long_Name.base_name fname, ftype,
-                      abstract_over (atom,
-                                     absfree(aname,atype, case_tm))),
+                      abstract_over (atom, absfree (aname,atype) case_tm)),
      pats = patts2}
 end end;
 
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/hologic.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -183,7 +183,7 @@
   | dest_set t = raise TERM ("dest_set", [t]);
 
 fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
-fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
+fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t;
 
 fun mk_mem (x, A) =
   let val setT = fastype_of A in
@@ -258,11 +258,11 @@
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
-fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
+fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
 
 fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
-fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
+fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
 
 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
 
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -871,7 +871,7 @@
 
 fun test_term ctxt [(t, [])] =
       let
-        val t' = list_abs_free (Term.add_frees t [], t)
+        val t' = fold_rev absfree (Term.add_frees t []) t;
         val thy = Proof_Context.theory_of ctxt;
         val (xs, p) = strip_abs t';
         val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -190,10 +190,11 @@
       | fun_of ts rts args used [] =
           let val xs = rev (rts @ ts)
           in if conclT = Extraction.nullT
-            then list_abs_free (map dest_Free xs, HOLogic.unit)
-            else list_abs_free (map dest_Free xs, list_comb
-              (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
-                map fastype_of (rev args) ---> conclT), rev args))
+            then fold_rev (absfree o dest_Free) xs HOLogic.unit
+            else fold_rev (absfree o dest_Free) xs
+              (list_comb
+                (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
+                  map fastype_of (rev args) ---> conclT), rev args))
           end
 
   in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
@@ -223,10 +224,11 @@
         let
           val Type ("fun", [U, _]) = T;
           val a :: names' = names
-        in (list_abs_free (("x", U) :: map_filter (fn intr =>
-          Option.map (pair (name_of_fn intr))
-            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
-          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
+        in
+          (fold_rev absfree (("x", U) :: map_filter (fn intr =>
+            Option.map (pair (name_of_fn intr))
+              (AList.lookup (op =) frees (name_of_fn intr))) intrs)
+            (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
         end
       end) concls rec_names)
   end;
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -207,7 +207,7 @@
                 val eqs' = map reverse_bounds eqs
                 val pat_eq' = reverse_bounds pat_eq
                 val inner_t =
-                  fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t))
+                  fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy T t)
                     (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
                 val lhs = term_of redex
                 val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -154,8 +154,8 @@
             val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
               (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
                 handle PrimrecError (s, NONE) => primrec_error_eqn s eq
-          in (fnames'', fnss'',
-              (list_abs_free (cargs' @ subs @ ls @ rs, rhs')) :: fns)
+          in
+            (fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns)
           end)
 
   in
diff -r 4b1a63678839 -r 7943b69f0188 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -318,10 +318,9 @@
         fun liftvar (Var ((a,j), T)) =
               Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
           | liftvar t = raise TERM("Variable expected", [t]);
-        fun liftterm t = list_abs_free
-              (param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t)
-        fun liftpair (cv,ct) =
-              (cterm_fun liftvar cv, cterm_fun liftterm ct)
+        fun liftterm t =
+          fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
+        fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
         val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate_normalize
               (map lifttvar envT', map liftpair cenv)
diff -r 4b1a63678839 -r 7943b69f0188 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -125,13 +125,13 @@
 fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
 
-fun absfree_proper (x, T, t) =
+fun absfree_proper (x, T) t =
   if can Name.dest_internal x
   then error ("Illegal internal variable in abstraction: " ^ quote x)
-  else Term.absfree (x, T, t);
+  else absfree (x, T) t;
 
-fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
-  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
+fun abs_tr [Free x, t] = absfree_proper x t
+  | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
   | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
       Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   | abs_tr ts = raise TERM ("abs_tr", ts);
diff -r 4b1a63678839 -r 7943b69f0188 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Pure/primitive_defs.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -74,7 +74,7 @@
     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
     val (lhs', args) = Term.strip_comb lhs;
-    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
+    val rhs' = fold_rev (absfree o dest_Free) args rhs;
   in (lhs', rhs') end;
 
 end;
diff -r 4b1a63678839 -r 7943b69f0188 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Pure/term.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -95,9 +95,8 @@
   val subst_free: (term * term) list -> term -> term
   val abstract_over: term * term -> term
   val lambda: term -> term -> term
-  val absfree: string * typ * term -> term
-  val absdummy: typ * term -> term
-  val list_abs_free: (string * typ) list * term -> term
+  val absfree: string * typ -> term -> term
+  val absdummy: typ -> term -> term
   val list_all_free: (string * typ) list * term -> term
   val list_all: (string * typ) list * term -> term
   val subst_atomic: (term * term) list -> term -> term
@@ -760,24 +759,18 @@
 
 fun lambda v t = lambda_name ("", v) t;
 
-(*Form an abstraction over a free variable.*)
-fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
-fun absdummy (T, body) = Abs (Name.uu_, T, body);
-
-(*Abstraction over a list of free variables*)
-fun list_abs_free ([ ] ,     t) = t
-  | list_abs_free ((a,T)::vars, t) =
-      absfree(a, T, list_abs_free(vars,t));
+fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
+fun absdummy T body = Abs (Name.uu_, T, body);
 
 (*Quantification over a list of free variables*)
 fun list_all_free ([], t: term) = t
   | list_all_free ((a,T)::vars, t) =
-        (all T) $ (absfree(a, T, list_all_free(vars,t)));
+        all T $ absfree (a, T) (list_all_free (vars, t));
 
 (*Quantification over a list of variables (already bound in body) *)
 fun list_all ([], t) = t
   | list_all ((a,T)::vars, t) =
-        (all T) $ (Abs(a, T, list_all(vars,t)));
+        all T $ Abs (a, T, list_all (vars, t));
 
 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
diff -r 4b1a63678839 -r 7943b69f0188 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Tools/induct.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -658,7 +658,7 @@
     fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
       | goal_concl 0 xs B =
           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
-          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
+          else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
       | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
       | goal_concl _ _ _ = NONE;
   in
diff -r 4b1a63678839 -r 7943b69f0188 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -235,7 +235,7 @@
       Misc_Legacy.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
-           absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
+           absfree ("rec", @{typ i}) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
 
diff -r 4b1a63678839 -r 7943b69f0188 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -127,8 +127,8 @@
   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
 
   val fp_abs =
-    absfree (X', Ind_Syntax.iT,
-        Ind_Syntax.mk_Collect (z', dom_sum,
+    absfree (X', Ind_Syntax.iT)
+        (Ind_Syntax.mk_Collect (z', dom_sum,
             Balanced_Tree.make FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
diff -r 4b1a63678839 -r 7943b69f0188 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -105,8 +105,8 @@
     val cnames         = map (#1 o dest_Const) constructors
     and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
 
-    fun absterm (Free(a,T), body) = absfree (a,T,body)
-      | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
+    fun absterm (Free x, body) = absfree x body
+      | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
 
     (*Translate rec equations into function arguments suitable for recursor.
       Missing cases are replaced by 0 and all cases are put into order.*)
diff -r 4b1a63678839 -r 7943b69f0188 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/ZF/ind_syntax.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -26,7 +26,7 @@
       Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
                    Term.betapply(P, Bound 0));
 
-fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
+fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =