modernized signature of Term.absfree/absdummy;
authorwenzelm
Wed Aug 17 18:05:31 2011 +0200 (2011-08-17)
changeset 442417943b69f0188
parent 44240 4b1a63678839
child 44245 45fb4b29c267
child 44250 9133bc634d9c
modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;
src/CCL/Term.thy
src/FOL/fologic.ML
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/Hoare/Separation.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Set.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/SMT/z3_model.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/list_to_set_comprehension.ML
src/HOL/Tools/primrec.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/primitive_defs.ML
src/Pure/term.ML
src/Tools/induct.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/CCL/Term.thy	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/CCL/Term.thy	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -58,18 +58,18 @@
     1.4  (* FIXME does not handle "_idtdummy" *)
     1.5  (* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
     1.6  
     1.7 -fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
     1.8 +fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
     1.9  fun let_tr' [a,Abs(id,T,b)] =
    1.10       let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
    1.11       in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
    1.12  
    1.13 -fun letrec_tr [Free(f,S),Free(x,T),a,b] =
    1.14 -      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
    1.15 -fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
    1.16 -      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
    1.17 -fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
    1.18 -      Const(@{const_syntax letrec3},dummyT) $
    1.19 -        absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
    1.20 +fun letrec_tr [Free f, Free x, a, b] =
    1.21 +      Const(@{const_syntax letrec}, dummyT) $ absfree x (absfree f a) $ absfree f b;
    1.22 +fun letrec2_tr [Free f, Free x, Free y, a, b] =
    1.23 +      Const(@{const_syntax letrec2}, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
    1.24 +fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
    1.25 +      Const(@{const_syntax letrec3}, dummyT) $
    1.26 +        absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
    1.27  
    1.28  fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
    1.29       let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
     2.1 --- a/src/FOL/fologic.ML	Wed Aug 17 16:46:58 2011 +0200
     2.2 +++ b/src/FOL/fologic.ML	Wed Aug 17 18:05:31 2011 +0200
     2.3 @@ -76,10 +76,10 @@
     2.4    | dest_eq t = raise TERM ("dest_eq", [t])
     2.5  
     2.6  fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
     2.7 -fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
     2.8 +fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
     2.9  
    2.10  fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
    2.11 -fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    2.12 +fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
    2.13  
    2.14  
    2.15  (* binary oprations and relations *)
     3.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Aug 17 16:46:58 2011 +0200
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Aug 17 18:05:31 2011 +0200
     3.3 @@ -393,7 +393,7 @@
     3.4      quant "forall" HOLogic.all_const ||
     3.5      quant "exists" HOLogic.exists_const ||
     3.6      scan_fail "illegal quantifier kind"
     3.7 -  fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
     3.8 +  fun mk_quant q (x, T) t = q T $ absfree (x, T) t
     3.9  
    3.10    val patternT = @{typ "SMT.pattern"}
    3.11    fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
     4.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Aug 17 16:46:58 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed Aug 17 18:05:31 2011 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4  (* building terms *)
     4.5  
     4.6  fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT)
     4.7 -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P)
     4.8 +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
     4.9  
    4.10  fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT)
    4.11  
     5.1 --- a/src/HOL/Hoare/Separation.thy	Wed Aug 17 16:46:58 2011 +0200
     5.2 +++ b/src/HOL/Hoare/Separation.thy	Wed Aug 17 18:05:31 2011 +0200
     5.3 @@ -68,11 +68,11 @@
     5.4  fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
     5.5    | singl_tr ts = raise TERM ("singl_tr", ts);
     5.6  fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
     5.7 -      absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
     5.8 +      absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $
     5.9        Syntax.free "H"
    5.10    | star_tr ts = raise TERM ("star_tr", ts);
    5.11  fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
    5.12 -      absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
    5.13 +      absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H"
    5.14    | wand_tr ts = raise TERM ("wand_tr", ts);
    5.15  *}
    5.16  
     6.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 16:46:58 2011 +0200
     6.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 18:05:31 2011 +0200
     6.3 @@ -28,17 +28,21 @@
     6.4  
     6.5  (** abstraction of body over a tuple formed from a list of free variables.
     6.6  Types are also built **)
     6.7 -fun mk_abstupleC []     body = absfree ("x", HOLogic.unitT, body)
     6.8 -  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
     6.9 -                               in if w=[] then absfree (n, T, body)
    6.10 -        else let val z  = mk_abstupleC w body;
    6.11 -                 val T2 = case z of Abs(_,T,_) => T
    6.12 -                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    6.13 -       in
    6.14 +fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
    6.15 +  | mk_abstupleC [v] body = absfree (dest_Free v) body
    6.16 +  | mk_abstupleC (v :: w) body =
    6.17 +      let
    6.18 +        val (x, T) = dest_Free v;
    6.19 +        val z = mk_abstupleC w body;
    6.20 +        val T2 =
    6.21 +          (case z of
    6.22 +            Abs (_, T, _) => T
    6.23 +          | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
    6.24 +      in
    6.25          Const (@{const_name prod_case},
    6.26 -          (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT)
    6.27 -            $ absfree (n, T, z)
    6.28 -       end end;
    6.29 +            (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
    6.30 +          absfree (x, T) z
    6.31 +      end;
    6.32  
    6.33  (** maps [x1,...,xn] to (x1,...,xn) and types**)
    6.34  fun mk_bodyC []      = HOLogic.unit
     7.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 17 16:46:58 2011 +0200
     7.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 17 18:05:31 2011 +0200
     7.3 @@ -102,16 +102,16 @@
     7.4      let
     7.5        val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
     7.6      in
     7.7 -      absdummy (@{typ nat}, absdummy (@{typ nat},
     7.8 -        Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
     7.9 +      absdummy @{typ nat} (absdummy @{typ nat}
    7.10 +        (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
    7.11            (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
    7.12            Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
    7.13            Predicate_Compile_Aux.mk_single compfuns
    7.14            (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
    7.15      end
    7.16    fun enumerate_addups_nat compfuns (_ : typ) =
    7.17 -    absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
    7.18 -    (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
    7.19 +    absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
    7.20 +    (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $
    7.21        (@{term "Code_Numeral.nat_of"} $ Bound 0) $
    7.22        (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
    7.23        @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
    7.24 @@ -120,8 +120,8 @@
    7.25        val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
    7.26        val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
    7.27      in
    7.28 -      absdummy(@{typ nat}, absdummy (@{typ nat},
    7.29 -        Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
    7.30 +      absdummy @{typ nat} (absdummy @{typ nat}
    7.31 +        (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
    7.32            (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
    7.33            (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
    7.34              @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 17 16:46:58 2011 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 17 18:05:31 2011 +0200
     8.3 @@ -1678,7 +1678,7 @@
     8.4                fresh_fs @
     8.5            map (fn (((P, T), (x, U)), Q) =>
     8.6             (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
     8.7 -            Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
     8.8 +            Abs ("z", HOLogic.unitT, absfree (x, U) Q)))
     8.9                (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
    8.10            map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
    8.11              rec_unique_frees)) induct_aux;
    8.12 @@ -2017,9 +2017,9 @@
    8.13            (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
    8.14            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    8.15        |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    8.16 -          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
    8.17 -           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    8.18 -             set $ Free ("x", T) $ Free ("y", T'))))))
    8.19 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T)
    8.20 +           (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
    8.21 +             (set $ Free ("x", T) $ Free ("y", T'))))))
    8.22                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
    8.23  
    8.24      (* prove characteristic equations for primrec combinators *)
     9.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 17 16:46:58 2011 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 17 18:05:31 2011 +0200
     9.3 @@ -187,7 +187,7 @@
     9.4          fun mk s =
     9.5            let
     9.6              val t = Syntax.read_term ctxt' s;
     9.7 -            val t' = list_abs_free (params, t) |>
     9.8 +            val t' = fold_rev absfree params t |>
     9.9                funpow (length params) (fn Abs (_, _, t) => t)
    9.10            in (t', HOLogic.dest_setT (fastype_of t)) end
    9.11            handle TERM _ =>
    10.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 17 16:46:58 2011 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 17 18:05:31 2011 +0200
    10.3 @@ -163,8 +163,7 @@
    10.4                val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    10.5                  (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    10.6                    handle RecError s => primrec_eq_err lthy s eq
    10.7 -            in (fnames'', fnss'',
    10.8 -                (list_abs_free (cargs' @ subs, rhs'))::fns)
    10.9 +            in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns)
   10.10              end)
   10.11  
   10.12    in (case AList.lookup (op =) fnames i of
   10.13 @@ -209,8 +208,8 @@
   10.14      val used = map fst (fold Term.add_frees fs []);
   10.15      val x = (singleton (Name.variant_list used) "x", dummyT);
   10.16      val frees = ls @ x :: rs;
   10.17 -    val raw_rhs = list_abs_free (frees,
   10.18 -      list_comb (Const (rec_name, dummyT), fs @ [Free x]))
   10.19 +    val raw_rhs = fold_rev absfree frees
   10.20 +      (list_comb (Const (rec_name, dummyT), fs @ [Free x]))
   10.21      val def_name = Thm.def_name (Long_Name.base_name fname);
   10.22      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
   10.23      val SOME var = get_first (fn ((b, _), mx) =>
    11.1 --- a/src/HOL/Set.thy	Wed Aug 17 16:46:58 2011 +0200
    11.2 +++ b/src/HOL/Set.thy	Wed Aug 17 18:05:31 2011 +0200
    11.3 @@ -281,7 +281,7 @@
    11.4          val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
    11.5          val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
    11.6          val exP = ex_tr [idts, P];
    11.7 -      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
    11.8 +      in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
    11.9  
   11.10    in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
   11.11  *}
    12.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 17 16:46:58 2011 +0200
    12.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 17 18:05:31 2011 +0200
    12.3 @@ -323,7 +323,7 @@
    12.4          val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
    12.5          val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
    12.6          val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
    12.7 -        val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
    12.8 +        val f = fold_rev (absfree o dest_Free) (xs @ ys) (mk_univ_inj ts n i);
    12.9  
   12.10          val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
   12.11          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    13.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 17 16:46:58 2011 +0200
    13.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 17 18:05:31 2011 +0200
    13.3 @@ -201,10 +201,10 @@
    13.4        let
    13.5          val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
    13.6            Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
    13.7 -            absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
    13.8 +            absfree ("y", T2) (set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
    13.9                (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   13.10          val cert = cterm_of thy1
   13.11 -        val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
   13.12 +        val insts = map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
   13.13            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   13.14          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   13.15            (map cert insts)) induct;
   13.16 @@ -238,9 +238,9 @@
   13.17        |> (Global_Theory.add_defs false o map Thm.no_attributes)
   13.18            (map (fn ((((name, comb), set), T), T') =>
   13.19              (Binding.name (Long_Name.base_name name ^ "_def"),
   13.20 -              Logic.mk_equals (comb, absfree ("x", T,
   13.21 -               Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   13.22 -                 set $ Free ("x", T) $ Free ("y", T'))))))
   13.23 +              Logic.mk_equals (comb, absfree ("x", T)
   13.24 +               (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
   13.25 +                 (set $ Free ("x", T) $ Free ("y", T'))))))
   13.26                     (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   13.27        ||> Sign.parent_path
   13.28        ||> Theory.checkpoint;
   13.29 @@ -306,8 +306,7 @@
   13.30                val frees = take (length cargs) frees';
   13.31                val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
   13.32              in
   13.33 -             (free, list_abs_free (map dest_Free frees',
   13.34 -               list_comb (free, frees)))
   13.35 +              (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
   13.36              end) (constrs ~~ (1 upto length constrs)));
   13.37  
   13.38            val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
    14.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 17 16:46:58 2011 +0200
    14.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 17 18:05:31 2011 +0200
    14.3 @@ -145,7 +145,7 @@
    14.4        (case t1 of
    14.5          NONE =>
    14.6            (case flt (Misc_Legacy.term_frees t2) of
    14.7 -            [Free (s, T)] => SOME (absfree (s, T, t2))
    14.8 +            [Free (s, T)] => SOME (absfree (s, T) t2)
    14.9            | _ => NONE)
   14.10        | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
   14.11      val insts = map_filter (fn (t, u) =>
    15.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Aug 17 16:46:58 2011 +0200
    15.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Aug 17 18:05:31 2011 +0200
    15.3 @@ -56,9 +56,8 @@
    15.4                    val rT = nth (rec_result_Ts) i;
    15.5                    val vs' = filter_out is_unit vs;
    15.6                    val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
    15.7 -                  val f' = Envir.eta_contract (list_abs_free
    15.8 -                    (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
    15.9 -                      else HOLogic.unit));
   15.10 +                  val f' = Envir.eta_contract (fold_rev (absfree o dest_Free) vs
   15.11 +                    (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
   15.12                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
   15.13                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
   15.14                  end
    16.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 17 16:46:58 2011 +0200
    16.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 17 18:05:31 2011 +0200
    16.3 @@ -68,8 +68,8 @@
    16.4            val args = Misc_Legacy.term_frees body
    16.5            (* Forms a lambda-abstraction over the formal parameters *)
    16.6            val rhs =
    16.7 -            list_abs_free (map dest_Free args,
    16.8 -                           HOLogic.choice_const T $ beta_eta_in_abs_body body)
    16.9 +            fold_rev (absfree o dest_Free) args
   16.10 +              (HOLogic.choice_const T $ beta_eta_in_abs_body body)
   16.11              |> mk_old_skolem_term_wrapper
   16.12            val comb = list_comb (rhs, args)
   16.13          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    17.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 16:46:58 2011 +0200
    17.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 18:05:31 2011 +0200
    17.3 @@ -491,7 +491,7 @@
    17.4        case strip_comb flex of
    17.5          (Var (z as (_, T)), args) =>
    17.6          add_terms (Var z,
    17.7 -          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
    17.8 +          fold_rev absdummy (take (length args) (binder_types T)) rigid)
    17.9        | _ => I
   17.10      fun unify_potential_flex comb atom =
   17.11        if is_flex comb then unify_flex comb atom
   17.12 @@ -541,7 +541,7 @@
   17.13             if k > j then t else t $ u
   17.14           | (t, u) => t $ u)
   17.15        | repair t = t
   17.16 -    val t' = t |> repair |> fold (curry absdummy) (map snd params)
   17.17 +    val t' = t |> repair |> fold (absdummy o snd) params
   17.18      fun do_instantiate th =
   17.19        case Term.add_vars (prop_of th) []
   17.20             |> filter_out ((Meson_Clausify.is_zapped_var_name orf
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 16:46:58 2011 +0200
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 18:05:31 2011 +0200
    18.3 @@ -1555,7 +1555,7 @@
    18.4      else
    18.5        fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
    18.6    end
    18.7 -  |> curry absdummy dataT
    18.8 +  |> absdummy dataT
    18.9  
   18.10  fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
   18.11    let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   18.12 @@ -1968,7 +1968,7 @@
   18.13            discriminate_value hol_ctxt x y_var ::
   18.14            map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
   18.15            |> foldr1 s_conj
   18.16 -      in List.foldr absdummy core_t arg_Ts end
   18.17 +      in fold_rev absdummy arg_Ts core_t end
   18.18    in
   18.19      [HOLogic.mk_imp
   18.20         (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
    19.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Aug 17 16:46:58 2011 +0200
    19.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Aug 17 18:05:31 2011 +0200
    19.3 @@ -634,7 +634,7 @@
    19.4                    fun app f =
    19.5                      list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
    19.6                  in
    19.7 -                  List.foldr absdummy (connective $ app pos $ app neg) arg_Ts
    19.8 +                  fold_rev absdummy arg_Ts (connective $ app pos $ app neg)
    19.9                  end
   19.10              end
   19.11            else
    20.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 16:46:58 2011 +0200
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 18:05:31 2011 +0200
    20.3 @@ -1017,7 +1017,7 @@
    20.4  
    20.5  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    20.6    let
    20.7 -    val t' = list_abs_free (Term.add_frees t [], t)
    20.8 +    val t' = fold_rev absfree (Term.add_frees t []) t
    20.9      val options = code_options_of (Proof_Context.theory_of ctxt)
   20.10      val thy = Theory.copy (Proof_Context.theory_of ctxt)
   20.11      val ((((full_constname, constT), vs'), intro), thy1) =
    21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 16:46:58 2011 +0200
    21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Aug 17 18:05:31 2011 +0200
    21.3 @@ -914,7 +914,7 @@
    21.4              val Ts = binder_types (fastype_of f')
    21.5              val bs = map Bound ((length Ts - 1) downto 0)
    21.6            in
    21.7 -            fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
    21.8 +            fold_rev absdummy Ts (f $ (list_comb (f', bs)))
    21.9            end
   21.10          val fs' = map apply_f fs
   21.11          val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   21.12 @@ -949,7 +949,7 @@
   21.13        val T' = TFree (tname', HOLogic.typeS)
   21.14        val U = TFree (uname, HOLogic.typeS)
   21.15        val y = Free (yname, U)
   21.16 -      val f' = absdummy (U --> T', Bound 0 $ y)
   21.17 +      val f' = absdummy (U --> T') (Bound 0 $ y)
   21.18        val th' = Thm.certify_instantiate
   21.19          ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
   21.20           [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Aug 17 16:46:58 2011 +0200
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Aug 17 18:05:31 2011 +0200
    22.3 @@ -524,7 +524,7 @@
    22.4           Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
    22.5           @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) 
    22.6        in
    22.7 -        absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3)
    22.8 +        absdummy @{typ code_numeral} (small_lazy $ HOLogic.mk_number @{typ int} 3)
    22.9        end
   22.10      ),
   22.11    modify_funT = I,
   22.12 @@ -580,27 +580,29 @@
   22.13  
   22.14  (** specific rpred functions -- move them to the correct place in this file *)
   22.15  fun mk_Eval_of (P as (Free (f, _)), T) mode =
   22.16 -let
   22.17 -  fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
   22.18 -    let
   22.19 -      val (bs2, i') = mk_bounds T2 i 
   22.20 -      val (bs1, i'') = mk_bounds T1 i'
   22.21 -    in
   22.22 -      (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
   22.23 -    end
   22.24 -    | mk_bounds T i = (Bound i, i + 1)
   22.25 -  fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
   22.26 -  fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
   22.27 -    | mk_tuple tTs = foldr1 mk_prod tTs;
   22.28 -  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)))
   22.29 -    | mk_split_abs T t = absdummy (T, t)
   22.30 -  val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
   22.31 -  val (inargs, outargs) = split_mode mode args
   22.32 -  val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
   22.33 -  val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   22.34 -in
   22.35 -  fold_rev mk_split_abs (binder_types T) inner_term  
   22.36 -end
   22.37 +  let
   22.38 +    fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
   22.39 +          let
   22.40 +            val (bs2, i') = mk_bounds T2 i 
   22.41 +            val (bs1, i'') = mk_bounds T1 i'
   22.42 +          in
   22.43 +            (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
   22.44 +          end
   22.45 +      | mk_bounds T i = (Bound i, i + 1)
   22.46 +    fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
   22.47 +    fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
   22.48 +      | mk_tuple tTs = foldr1 mk_prod tTs
   22.49 +    fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
   22.50 +          absdummy T
   22.51 +            (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
   22.52 +      | mk_split_abs T t = absdummy T t
   22.53 +    val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
   22.54 +    val (inargs, outargs) = split_mode mode args
   22.55 +    val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
   22.56 +    val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   22.57 +  in
   22.58 +    fold_rev mk_split_abs (binder_types T) inner_term
   22.59 +  end
   22.60  
   22.61  fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
   22.62    let
   22.63 @@ -1831,7 +1833,7 @@
   22.64      val t' =
   22.65        if stats andalso compilation = New_Pos_Random_DSeq then
   22.66          mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
   22.67 -          (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
   22.68 +          (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
   22.69              @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
   22.70        else
   22.71          mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
    23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Aug 17 16:46:58 2011 +0200
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Aug 17 18:05:31 2011 +0200
    23.3 @@ -218,7 +218,7 @@
    23.4  
    23.5  fun compile_term compilation options ctxt t =
    23.6    let
    23.7 -    val t' = list_abs_free (Term.add_frees t [], t)
    23.8 +    val t' = fold_rev absfree (Term.add_frees t []) t
    23.9      val thy = Theory.copy (Proof_Context.theory_of ctxt)
   23.10      val ((((full_constname, constT), vs'), intro), thy1) =
   23.11        Predicate_Compile_Aux.define_quickcheck_predicate t' thy
   23.12 @@ -269,7 +269,7 @@
   23.13          | Pos_Generator_DSeq => mk_gen_bind (prog,
   23.14              mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
   23.15              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
   23.16 -        | Depth_Limited_Random => fold_rev (curry absdummy)
   23.17 +        | Depth_Limited_Random => fold_rev absdummy
   23.18              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
   23.19               @{typ "code_numeral * code_numeral"}]
   23.20              (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
    24.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Aug 17 16:46:58 2011 +0200
    24.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Aug 17 18:05:31 2011 +0200
    24.3 @@ -70,7 +70,7 @@
    24.4    end
    24.5  
    24.6  fun mk_unit_let (x, y) =
    24.7 -  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
    24.8 +  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
    24.9    
   24.10  (* handling inductive datatypes *)
   24.11  
   24.12 @@ -113,14 +113,14 @@
   24.13      map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   24.14    end
   24.15  
   24.16 -fun gen_mk_call c T =  (T, fn t => c T $ absdummy (T, t) $ size_pred)
   24.17 +fun gen_mk_call c T =  (T, fn t => c T $ absdummy T t $ size_pred)
   24.18  
   24.19  fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
   24.20    let
   24.21      val T = Type (tyco, Ts)
   24.22      val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   24.23    in
   24.24 -   (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
   24.25 +   (T, fn t => nth functerms k $ absdummy T t $ size_pred)
   24.26    end
   24.27  
   24.28  fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
   24.29 @@ -184,18 +184,18 @@
   24.30            Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
   24.31              full_exhaustiveT T)
   24.32        in
   24.33 -        (T, (fn t => full_exhaustive $
   24.34 +        (T, fn t => full_exhaustive $
   24.35            (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   24.36 -          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   24.37 +          $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   24.38        end
   24.39      fun mk_aux_call fTs (k, _) (tyco, Ts) =
   24.40        let
   24.41          val T = Type (tyco, Ts)
   24.42          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   24.43        in
   24.44 -        (T, (fn t => nth functerms k $
   24.45 +        (T, fn t => nth functerms k $
   24.46            (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   24.47 -            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   24.48 +            $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   24.49        end
   24.50      fun mk_consexpr simpleT (c, xs) =
   24.51        let
   24.52 @@ -209,7 +209,7 @@
   24.53            bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   24.54          val start_term = test_function simpleT $ 
   24.55          (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   24.56 -          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   24.57 +          $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
   24.58        in fold_rev (fn f => fn t => f t) fns start_term end
   24.59      fun mk_rhs exprs =
   24.60          @{term "If :: bool => term list option => term list option => term list option"}
   24.61 @@ -382,7 +382,7 @@
   24.62  
   24.63  fun mk_parametric_generator_expr mk_generator_expr =
   24.64    Quickcheck_Common.gen_mk_parametric_generator_expr 
   24.65 -    ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
   24.66 +    ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: term list option"}),
   24.67        @{typ "code_numeral => term list option"})
   24.68  
   24.69  fun mk_validator_expr ctxt t =
   24.70 @@ -412,9 +412,9 @@
   24.71      val return = @{term "Some :: term list => term list option"} $
   24.72        (HOLogic.mk_list @{typ "term"}
   24.73          (replicate (length frees + length eval_terms) dummy_term))
   24.74 -    val wrap = absdummy (@{typ bool},
   24.75 -      @{term "If :: bool => term list option => term list option => term list option"} $
   24.76 -      Bound 0 $ @{term "None :: term list option"} $ return)
   24.77 +    val wrap = absdummy @{typ bool}
   24.78 +      (@{term "If :: bool => term list option => term list option => term list option"} $
   24.79 +        Bound 0 $ @{term "None :: term list option"} $ return)
   24.80    in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   24.81    
   24.82  (** generator compiliation **)
    25.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 16:46:58 2011 +0200
    25.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 18:05:31 2011 +0200
    25.3 @@ -340,10 +340,11 @@
    25.4        in
    25.5          case dT of
    25.6            Type (@{type_name fun}, _) =>
    25.7 -            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    25.8 -            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
    25.9 -        | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   25.10 -            Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
   25.11 +            (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   25.12 +              Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
   25.13 +        | _ =>
   25.14 +            (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   25.15 +              Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
   25.16        end
   25.17        | eval_function T = (I, T)
   25.18      val (tt, boundTs') = split_list (map eval_function boundTs)
   25.19 @@ -432,7 +433,7 @@
   25.20        end
   25.21      else
   25.22        let
   25.23 -        val t' = Term.list_abs_free (Term.add_frees t [], t)
   25.24 +        val t' = fold_rev absfree (Term.add_frees t []) t
   25.25          fun wrap f t = list_abs (f (strip_abs t))
   25.26          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   25.27          fun ensure_testable t =
    26.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 16:46:58 2011 +0200
    26.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 18:05:31 2011 +0200
    26.3 @@ -112,7 +112,7 @@
    26.4        if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
    26.5          (mk_generator_expr ctxt (t, eval_terms)) $ else_t
    26.6    in
    26.7 -    absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
    26.8 +    absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
    26.9    end
   26.10  
   26.11  (** post-processing of function terms **)
    27.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Aug 17 16:46:58 2011 +0200
    27.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Aug 17 18:05:31 2011 +0200
    27.3 @@ -291,7 +291,7 @@
    27.4  fun mk_generator_expr ctxt (t, eval_terms) =
    27.5    let  
    27.6      val thy = Proof_Context.theory_of ctxt
    27.7 -    val prop = list_abs_free (Term.add_frees t [], t)
    27.8 +    val prop = fold_rev absfree (Term.add_frees t []) t
    27.9      val Ts = (map snd o fst o strip_abs) prop
   27.10      val bound_max = length Ts - 1;
   27.11      val bounds = map_index (fn (i, ty) =>
   27.12 @@ -317,7 +317,7 @@
   27.13  fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   27.14    let
   27.15      val thy = Proof_Context.theory_of ctxt
   27.16 -    val prop = list_abs_free (Term.add_frees t [], t)
   27.17 +    val prop = fold_rev absfree (Term.add_frees t []) t
   27.18      val Ts = (map snd o fst o strip_abs) prop
   27.19      val bound_max = length Ts - 1
   27.20      val bounds = map_index (fn (i, ty) =>
   27.21 @@ -360,13 +360,13 @@
   27.22  
   27.23  val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   27.24    ((mk_generator_expr, 
   27.25 -    absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
   27.26 +    absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => term list option * Random.seed"}),
   27.27      @{typ "code_numeral => Random.seed => term list option * Random.seed"})
   27.28  
   27.29  val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   27.30    ((mk_reporting_generator_expr,
   27.31 -    absdummy (@{typ code_numeral},
   27.32 -      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
   27.33 +    absdummy @{typ code_numeral}
   27.34 +      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"}),
   27.35      @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
   27.36      
   27.37      
    28.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Wed Aug 17 16:46:58 2011 +0200
    28.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Aug 17 18:05:31 2011 +0200
    28.3 @@ -156,11 +156,11 @@
    28.4          val (dT', rT') = Term.dest_funT rT
    28.5        in
    28.6          mk_fun_upd dT rT $ f $ t $
    28.7 -          mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
    28.8 +          mk_update (ts, u) (absdummy dT' (Const ("_", rT')))
    28.9        end
   28.10  
   28.11  fun mk_lambda Ts (t, pats) =
   28.12 -  fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
   28.13 +  fold_rev absdummy Ts t |> fold mk_update pats
   28.14  
   28.15  fun translate ((t, k), (e, cs)) =
   28.16    let
    29.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 17 16:46:58 2011 +0200
    29.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Aug 17 18:05:31 2011 +0200
    29.3 @@ -145,7 +145,7 @@
    29.4      val frees = map Free (Term.add_frees t [])
    29.5      val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
    29.6      val vs = map (Term.dest_Free o Thm.term_of) cvs'
    29.7 -  in (Term.list_abs_free (vs, t), cvs') end
    29.8 +  in (fold_rev absfree vs t, cvs') end
    29.9  
   29.10  fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
   29.11    let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
    30.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 16:46:58 2011 +0200
    30.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 18:05:31 2011 +0200
    30.3 @@ -342,8 +342,7 @@
    30.4   ("The following clauses are redundant (covered by preceding clauses): " ^
    30.5                     commas (map (fn i => string_of_int (i + 1)) L))
    30.6   in {functional = Abs(Long_Name.base_name fname, ftype,
    30.7 -                      abstract_over (atom,
    30.8 -                                     absfree(aname,atype, case_tm))),
    30.9 +                      abstract_over (atom, absfree (aname,atype) case_tm)),
   30.10       pats = patts2}
   30.11  end end;
   30.12  
    31.1 --- a/src/HOL/Tools/hologic.ML	Wed Aug 17 16:46:58 2011 +0200
    31.2 +++ b/src/HOL/Tools/hologic.ML	Wed Aug 17 18:05:31 2011 +0200
    31.3 @@ -183,7 +183,7 @@
    31.4    | dest_set t = raise TERM ("dest_set", [t]);
    31.5  
    31.6  fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
    31.7 -fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    31.8 +fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t;
    31.9  
   31.10  fun mk_mem (x, A) =
   31.11    let val setT = fastype_of A in
   31.12 @@ -258,11 +258,11 @@
   31.13    | dest_eq t = raise TERM ("dest_eq", [t])
   31.14  
   31.15  fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
   31.16 -fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
   31.17 +fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
   31.18  fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
   31.19  
   31.20  fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
   31.21 -fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   31.22 +fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
   31.23  
   31.24  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
   31.25  
    32.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 16:46:58 2011 +0200
    32.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 18:05:31 2011 +0200
    32.3 @@ -871,7 +871,7 @@
    32.4  
    32.5  fun test_term ctxt [(t, [])] =
    32.6        let
    32.7 -        val t' = list_abs_free (Term.add_frees t [], t)
    32.8 +        val t' = fold_rev absfree (Term.add_frees t []) t;
    32.9          val thy = Proof_Context.theory_of ctxt;
   32.10          val (xs, p) = strip_abs t';
   32.11          val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
    33.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Aug 17 16:46:58 2011 +0200
    33.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Aug 17 18:05:31 2011 +0200
    33.3 @@ -190,10 +190,11 @@
    33.4        | fun_of ts rts args used [] =
    33.5            let val xs = rev (rts @ ts)
    33.6            in if conclT = Extraction.nullT
    33.7 -            then list_abs_free (map dest_Free xs, HOLogic.unit)
    33.8 -            else list_abs_free (map dest_Free xs, list_comb
    33.9 -              (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
   33.10 -                map fastype_of (rev args) ---> conclT), rev args))
   33.11 +            then fold_rev (absfree o dest_Free) xs HOLogic.unit
   33.12 +            else fold_rev (absfree o dest_Free) xs
   33.13 +              (list_comb
   33.14 +                (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
   33.15 +                  map fastype_of (rev args) ---> conclT), rev args))
   33.16            end
   33.17  
   33.18    in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
   33.19 @@ -223,10 +224,11 @@
   33.20          let
   33.21            val Type ("fun", [U, _]) = T;
   33.22            val a :: names' = names
   33.23 -        in (list_abs_free (("x", U) :: map_filter (fn intr =>
   33.24 -          Option.map (pair (name_of_fn intr))
   33.25 -            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   33.26 -          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
   33.27 +        in
   33.28 +          (fold_rev absfree (("x", U) :: map_filter (fn intr =>
   33.29 +            Option.map (pair (name_of_fn intr))
   33.30 +              (AList.lookup (op =) frees (name_of_fn intr))) intrs)
   33.31 +            (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
   33.32          end
   33.33        end) concls rec_names)
   33.34    end;
    34.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML	Wed Aug 17 16:46:58 2011 +0200
    34.2 +++ b/src/HOL/Tools/list_to_set_comprehension.ML	Wed Aug 17 18:05:31 2011 +0200
    34.3 @@ -207,7 +207,7 @@
    34.4                  val eqs' = map reverse_bounds eqs
    34.5                  val pat_eq' = reverse_bounds pat_eq
    34.6                  val inner_t =
    34.7 -                  fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t))
    34.8 +                  fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy T t)
    34.9                      (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   34.10                  val lhs = term_of redex
   34.11                  val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
    35.1 --- a/src/HOL/Tools/primrec.ML	Wed Aug 17 16:46:58 2011 +0200
    35.2 +++ b/src/HOL/Tools/primrec.ML	Wed Aug 17 18:05:31 2011 +0200
    35.3 @@ -154,8 +154,8 @@
    35.4              val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    35.5                (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    35.6                  handle PrimrecError (s, NONE) => primrec_error_eqn s eq
    35.7 -          in (fnames'', fnss'',
    35.8 -              (list_abs_free (cargs' @ subs @ ls @ rs, rhs')) :: fns)
    35.9 +          in
   35.10 +            (fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns)
   35.11            end)
   35.12  
   35.13    in
    36.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Aug 17 16:46:58 2011 +0200
    36.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Aug 17 18:05:31 2011 +0200
    36.3 @@ -318,10 +318,9 @@
    36.4          fun liftvar (Var ((a,j), T)) =
    36.5                Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
    36.6            | liftvar t = raise TERM("Variable expected", [t]);
    36.7 -        fun liftterm t = list_abs_free
    36.8 -              (param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t)
    36.9 -        fun liftpair (cv,ct) =
   36.10 -              (cterm_fun liftvar cv, cterm_fun liftterm ct)
   36.11 +        fun liftterm t =
   36.12 +          fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
   36.13 +        fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
   36.14          val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
   36.15          val rule = Drule.instantiate_normalize
   36.16                (map lifttvar envT', map liftpair cenv)
    37.1 --- a/src/Pure/Syntax/syntax_trans.ML	Wed Aug 17 16:46:58 2011 +0200
    37.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Wed Aug 17 18:05:31 2011 +0200
    37.3 @@ -125,13 +125,13 @@
    37.4  fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
    37.5    | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
    37.6  
    37.7 -fun absfree_proper (x, T, t) =
    37.8 +fun absfree_proper (x, T) t =
    37.9    if can Name.dest_internal x
   37.10    then error ("Illegal internal variable in abstraction: " ^ quote x)
   37.11 -  else Term.absfree (x, T, t);
   37.12 +  else absfree (x, T) t;
   37.13  
   37.14 -fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
   37.15 -  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
   37.16 +fun abs_tr [Free x, t] = absfree_proper x t
   37.17 +  | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
   37.18    | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
   37.19        Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   37.20    | abs_tr ts = raise TERM ("abs_tr", ts);
    38.1 --- a/src/Pure/primitive_defs.ML	Wed Aug 17 16:46:58 2011 +0200
    38.2 +++ b/src/Pure/primitive_defs.ML	Wed Aug 17 18:05:31 2011 +0200
    38.3 @@ -74,7 +74,7 @@
    38.4      val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    38.5      val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
    38.6      val (lhs', args) = Term.strip_comb lhs;
    38.7 -    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    38.8 +    val rhs' = fold_rev (absfree o dest_Free) args rhs;
    38.9    in (lhs', rhs') end;
   38.10  
   38.11  end;
    39.1 --- a/src/Pure/term.ML	Wed Aug 17 16:46:58 2011 +0200
    39.2 +++ b/src/Pure/term.ML	Wed Aug 17 18:05:31 2011 +0200
    39.3 @@ -95,9 +95,8 @@
    39.4    val subst_free: (term * term) list -> term -> term
    39.5    val abstract_over: term * term -> term
    39.6    val lambda: term -> term -> term
    39.7 -  val absfree: string * typ * term -> term
    39.8 -  val absdummy: typ * term -> term
    39.9 -  val list_abs_free: (string * typ) list * term -> term
   39.10 +  val absfree: string * typ -> term -> term
   39.11 +  val absdummy: typ -> term -> term
   39.12    val list_all_free: (string * typ) list * term -> term
   39.13    val list_all: (string * typ) list * term -> term
   39.14    val subst_atomic: (term * term) list -> term -> term
   39.15 @@ -760,24 +759,18 @@
   39.16  
   39.17  fun lambda v t = lambda_name ("", v) t;
   39.18  
   39.19 -(*Form an abstraction over a free variable.*)
   39.20 -fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
   39.21 -fun absdummy (T, body) = Abs (Name.uu_, T, body);
   39.22 -
   39.23 -(*Abstraction over a list of free variables*)
   39.24 -fun list_abs_free ([ ] ,     t) = t
   39.25 -  | list_abs_free ((a,T)::vars, t) =
   39.26 -      absfree(a, T, list_abs_free(vars,t));
   39.27 +fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
   39.28 +fun absdummy T body = Abs (Name.uu_, T, body);
   39.29  
   39.30  (*Quantification over a list of free variables*)
   39.31  fun list_all_free ([], t: term) = t
   39.32    | list_all_free ((a,T)::vars, t) =
   39.33 -        (all T) $ (absfree(a, T, list_all_free(vars,t)));
   39.34 +        all T $ absfree (a, T) (list_all_free (vars, t));
   39.35  
   39.36  (*Quantification over a list of variables (already bound in body) *)
   39.37  fun list_all ([], t) = t
   39.38    | list_all ((a,T)::vars, t) =
   39.39 -        (all T) $ (Abs(a, T, list_all(vars,t)));
   39.40 +        all T $ Abs (a, T, list_all (vars, t));
   39.41  
   39.42  (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   39.43    A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
    40.1 --- a/src/Tools/induct.ML	Wed Aug 17 16:46:58 2011 +0200
    40.2 +++ b/src/Tools/induct.ML	Wed Aug 17 18:05:31 2011 +0200
    40.3 @@ -658,7 +658,7 @@
    40.4      fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
    40.5        | goal_concl 0 xs B =
    40.6            if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
    40.7 -          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
    40.8 +          else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
    40.9        | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
   40.10        | goal_concl _ _ _ = NONE;
   40.11    in
    41.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Aug 17 16:46:58 2011 +0200
    41.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Aug 17 18:05:31 2011 +0200
    41.3 @@ -235,7 +235,7 @@
    41.4        Misc_Legacy.mk_defpair
    41.5          (recursor_tm,
    41.6           @{const Univ.Vrecursor} $
    41.7 -           absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
    41.8 +           absfree ("rec", @{typ i}) (list_comb (case_const, recursor_cases)));
    41.9  
   41.10    (* Build the new theory *)
   41.11  
    42.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Aug 17 16:46:58 2011 +0200
    42.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 17 18:05:31 2011 +0200
    42.3 @@ -127,8 +127,8 @@
    42.4    val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
    42.5  
    42.6    val fp_abs =
    42.7 -    absfree (X', Ind_Syntax.iT,
    42.8 -        Ind_Syntax.mk_Collect (z', dom_sum,
    42.9 +    absfree (X', Ind_Syntax.iT)
   42.10 +        (Ind_Syntax.mk_Collect (z', dom_sum,
   42.11              Balanced_Tree.make FOLogic.mk_disj part_intrs));
   42.12  
   42.13    val fp_rhs = Fp.oper $ dom_sum $ fp_abs
    43.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Aug 17 16:46:58 2011 +0200
    43.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Aug 17 18:05:31 2011 +0200
    43.3 @@ -105,8 +105,8 @@
    43.4      val cnames         = map (#1 o dest_Const) constructors
    43.5      and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
    43.6  
    43.7 -    fun absterm (Free(a,T), body) = absfree (a,T,body)
    43.8 -      | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
    43.9 +    fun absterm (Free x, body) = absfree x body
   43.10 +      | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
   43.11  
   43.12      (*Translate rec equations into function arguments suitable for recursor.
   43.13        Missing cases are replaced by 0 and all cases are put into order.*)
    44.1 --- a/src/ZF/ind_syntax.ML	Wed Aug 17 16:46:58 2011 +0200
    44.2 +++ b/src/ZF/ind_syntax.ML	Wed Aug 17 18:05:31 2011 +0200
    44.3 @@ -26,7 +26,7 @@
    44.4        Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
    44.5                     Term.betapply(P, Bound 0));
    44.6  
    44.7 -fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
    44.8 +fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t;
    44.9  
   44.10  (*simple error-checking in the premises of an inductive definition*)
   44.11  fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =