# HG changeset patch
# User wenzelm
# Date 1301151322 -3600
# Node ID 524bb42442dce92d5a434a279bbc67e8cf2f0a43
# Parent  bb898647541672a3dad8da574df79a4d989ad61f# Parent  74bf78db0d877dff215a14344e1fbaf3286551c3
merged

diff -r bb8986475416 -r 524bb42442dc src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -46,7 +46,7 @@
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     fun mk_all ((s, T), (P,n)) =
-      if member (op =) (loose_bnos P) 0 then
+      if Term.is_dependent P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
diff -r bb8986475416 -r 524bb42442dc src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -51,7 +51,7 @@
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     fun mk_all ((s, T), (P,n)) =
-      if member (op =) (loose_bnos P) 0 then
+      if Term.is_dependent P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
diff -r bb8986475416 -r 524bb42442dc src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -66,7 +66,7 @@
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     fun mk_all ((s, T), (P,n)) =
-      if member (op =) (loose_bnos P) 0 then
+      if Term.is_dependent P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
diff -r bb8986475416 -r 524bb42442dc src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -23,9 +23,6 @@
 val cont_L = @{thm cont2cont_LAM}
 val cont_R = @{thm cont_Rep_cfun2}
 
-(* checks whether a term contains no dangling bound variables *)
-fun is_closed_term t = not (Term.loose_bvar (t, 0))
-
 (* checks whether a term is written entirely in the LCF sublanguage *)
 fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
@@ -34,7 +31,7 @@
   | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
       is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
-  | is_lcf_term t = is_closed_term t
+  | is_lcf_term t = not (Term.is_open t)
 
 (*
   efficiently generates a cont thm for every LAM abstraction in a term,
diff -r bb8986475416 -r 524bb42442dc src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 15:55:22 2011 +0100
@@ -93,20 +93,14 @@
           annquote_tr' (Syntax.const name) (r :: t :: ts)
       | annbexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
 
     fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | annassign_tr' _ = raise Match;
 
     fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
diff -r bb8986475416 -r 524bb42442dc src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 15:55:22 2011 +0100
@@ -67,15 +67,9 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r bb8986475416 -r 524bb42442dc src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 15:55:22 2011 +0100
@@ -237,15 +237,9 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun K_tr' (Abs (_, _, t)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
-          if null (loose_bnos t) then t else raise Match
-      | K_tr' _ = raise Match;
-
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r bb8986475416 -r 524bb42442dc src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Product_Type.thy	Sat Mar 26 15:55:22 2011 +0100
@@ -272,7 +272,7 @@
   fun contract Q f ts =
     case ts of
       [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
-      => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
+      => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
     | _ => f ts;
   fun contract2 (Q,f) = (Q, contract Q f);
   val pairs =
diff -r bb8986475416 -r 524bb42442dc src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -275,10 +275,10 @@
          fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
                let val (_::nT::_) = binder_types lT;
                          (*  ('v => 'a) => 'n => ('n => 'v) => 'a *)
-                   val x' = if not (loose_bvar1 (x,0))
+                   val x' = if not (Term.is_dependent x)
                             then Bound 1
                             else raise TERM ("",[x]);
-                   val n' = if not (loose_bvar1 (n,0))
+                   val n' = if not (Term.is_dependent n)
                             then Bound 2
                             else raise TERM ("",[n]);
                    val sel' = lo $ d $ n' $ s;
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -243,8 +243,8 @@
         val _ = length args > 0 orelse input_error "Function has no arguments:"
 
         fun add_bvs t is = add_loose_bnos (t, 0, is)
-            val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
-                        |> map (fst o nth (rev qs))
+        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
+                    |> map (fst o nth (rev qs))
 
         val _ = null rvs orelse input_error
           ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -87,7 +87,7 @@
          NONE => no_tac
        | SOME (arg, conv) =>
            let open Conv in
-              if not (null (loose_bnos arg)) then no_tac
+              if Term.is_open arg then no_tac
               else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                 THEN_ALL_NEW etac @{thm thin_rl}
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -125,8 +125,8 @@
         | Var _ => makeK()  (*though Var isn't expected*)
         | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
         | rator$rand =>
-            if loose_bvar1 (rator,0) then (*C or S*)
-               if loose_bvar1 (rand,0) then (*S*)
+            if Term.is_dependent rator then (*C or S*)
+               if Term.is_dependent rand then (*S*)
                  let val crator = cterm_of thy (Abs(x,xT,rator))
                      val crand = cterm_of thy (Abs(x,xT,rand))
                      val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
@@ -141,7 +141,7 @@
                  in
                    Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
                  end
-            else if loose_bvar1 (rand,0) then (*B or eta*)
+            else if Term.is_dependent rand then (*B or eta*)
                if rand = Bound 0 then Thm.eta_conversion ct
                else (*B*)
                  let val crand = cterm_of thy (Abs(x,xT,rand))
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -738,10 +738,10 @@
                   val ts2' = map
                     (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
                   val (ots, its) = List.partition is_Bound ts2;
-                  val no_loose = forall (fn t => not (loose_bvar (t, 0)))
+                  val closed = forall (not o Term.is_open)
                 in
                   if null (duplicates op = ots) andalso
-                    no_loose ts1 andalso no_loose its
+                    closed ts1 andalso closed its
                   then
                     let val (call_p, gr') = mk_ind_call thy defs dep module true
                       s T (ts1 @ ts2') names thyname k intrs gr 
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -40,7 +40,7 @@
              (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
-                  if not (loose_bvar (S', 0)) andalso
+                  if not (Term.is_open S') andalso
                     ts = map Bound (length ps downto 0)
                   then
                     let val simp = full_simp_tac (Simplifier.inherit_context ss
@@ -128,7 +128,7 @@
     fun eta b (Abs (a, T, body)) =
           (case eta b body of
              body' as (f $ Bound 0) =>
-               if loose_bvar1 (f, 0) orelse not b then Abs (a, T, body')
+               if Term.is_dependent f orelse not b then Abs (a, T, body')
                else incr_boundvars ~1 f
            | body' => Abs (a, T, body'))
       | eta b (t $ u) = eta b t $ eta (p (head_of t)) u
diff -r bb8986475416 -r 524bb42442dc src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -961,21 +961,11 @@
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
       (case dest_update ctxt c of
         SOME name =>
-          let
-            val opt_t =
-              (case k of
-                Abs (_, _, Abs (_, _, t) $ Bound 0) =>
-                  if null (loose_bnos t) then SOME t else NONE
-              | Abs (_, _, t) =>
-                  if null (loose_bnos t) then SOME t else NONE
-              | _ => NONE);
-          in
-            (case opt_t of
-              SOME t =>
-                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
-                  (field_updates_tr' ctxt u)
-            | NONE => ([], tm))
-          end
+          (case try Syntax.const_abs_tr' k of
+            SOME t =>
+              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
+                (field_updates_tr' ctxt u)
+          | NONE => ([], tm))
       | NONE => ([], tm))
   | field_updates_tr' _ tm = ([], tm);
 
diff -r bb8986475416 -r 524bb42442dc src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Provers/hypsubst.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -58,8 +58,6 @@
 
 exception EQ_VAR;
 
-fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
-
 (*Simplifier turns Bound variables to special Free variables:
   change it back (any Bound variable will do)*)
 fun contract t =
@@ -84,22 +82,24 @@
   if novars andalso (has_tvars t orelse has_tvars u)
   then raise Match   (*variables in the type!*)
   else
-  case (contract t, contract u) of
-       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
-                       then raise Match
-                       else true                (*eliminates t*)
-     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
-                       then raise Match
-                       else false               (*eliminates u*)
-     | (t' as Free _, _) => if bnd orelse Logic.occs(t',u) orelse
-                          novars andalso has_vars u
-                       then raise Match
-                       else true                (*eliminates t*)
-     | (_, u' as Free _) => if bnd orelse Logic.occs(u',t) orelse
-                          novars andalso has_vars t
-                       then raise Match
-                       else false               (*eliminates u*)
-     | _ => raise Match;
+    (case (contract t, contract u) of
+      (Bound i, _) =>
+        if loose_bvar1 (u, i) orelse novars andalso has_vars u
+        then raise Match
+        else true                (*eliminates t*)
+    | (_, Bound i) =>
+        if loose_bvar1 (t, i) orelse novars andalso has_vars t
+        then raise Match
+        else false               (*eliminates u*)
+    | (t' as Free _, _) =>
+        if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
+        then raise Match
+        else true                (*eliminates t*)
+    | (_, u' as Free _) =>
+        if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
+        then raise Match
+        else false               (*eliminates u*)
+    | _ => raise Match);
 
 (*Locates a substitutable variable on the left (resp. right) of an equality
    assumption.  Returns the number of intervening assumptions. *)
diff -r bb8986475416 -r 524bb42442dc src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -107,7 +107,7 @@
       | abs_body _ _ a = a;
     fun close (y, U) B =
       let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
-      in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
+      in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
     fun close_form A =
       let
         val occ_frees = rev (fold_aterms add_free A []);
diff -r bb8986475416 -r 524bb42442dc src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -10,10 +10,11 @@
   val eta_contract_raw: Config.raw
   val eta_contract: bool Config.T
   val atomic_abs_tr': string * typ * term -> term * term
+  val const_abs_tr': term -> term
+  val mk_binder_tr: string * string -> string * (term list -> term)
+  val mk_binder_tr': string * string -> string * (term list -> term)
   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
-  val mk_binder_tr: string * string -> string * (term list -> term)
-  val mk_binder_tr': string * string -> string * (term list -> term)
   val dependent_tr': string * string -> term list -> term
   val antiquote_tr: string -> term -> term
   val quote_tr: string -> term -> term
@@ -198,7 +199,8 @@
       if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
       else
         list_comb (c $ update_name_tr [t] $
-          (Lexicon.fun_type $ (Lexicon.fun_type $ ty $ ty) $ Lexicon.dummy_type), ts)
+          (Lexicon.fun_type $
+            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
   | update_name_tr ts = raise TERM ("update_name_tr", ts);
 
 
@@ -259,6 +261,28 @@
   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
 
 
+(* partial eta-contraction before printing *)
+
+fun eta_abs (Abs (a, T, t)) =
+      (case eta_abs t of
+        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
+      | t' as f $ u =>
+          (case eta_abs u of
+            Bound 0 =>
+              if Term.is_dependent f then Abs (a, T, t')
+              else incr_boundvars ~1 f
+          | _ => Abs (a, T, t'))
+      | t' => Abs (a, T, t'))
+  | eta_abs t = t;
+
+val eta_contract_default = Unsynchronized.ref true;
+val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract = Config.bool eta_contract_raw;
+
+fun eta_contr ctxt tm =
+  if Config.get ctxt eta_contract then eta_abs tm else tm;
+
+
 (* abstraction *)
 
 fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
@@ -273,39 +297,13 @@
     val body = body_of tm;
     val rev_new_vars = Term.rename_wrt_term body vars;
     fun subst (x, T) b =
-      if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
+      if can Name.dest_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
       else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
     val (rev_vars', body') = fold_map subst rev_new_vars body;
   in (rev rev_vars', body') end;
 
 
-(*do (partial) eta-contraction before printing*)
-
-val eta_contract_default = Unsynchronized.ref true;
-val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
-val eta_contract = Config.bool eta_contract_raw;
-
-fun eta_contr ctxt tm =
-  let
-    fun is_aprop (Const ("_aprop", _)) = true
-      | is_aprop _ = false;
-
-    fun eta_abs (Abs (a, T, t)) =
-          (case eta_abs t of
-            t' as f $ u =>
-              (case eta_abs u of
-                Bound 0 =>
-                  if Term.loose_bvar1 (f, 0) orelse is_aprop f then Abs (a, T, t')
-                  else  incr_boundvars ~1 f
-              | _ => Abs (a, T, t'))
-          | t' => Abs (a, T, t'))
-      | eta_abs t = t;
-  in
-    if Config.get ctxt eta_contract then eta_abs tm else tm
-  end;
-
-
 fun abs_tr' ctxt tm =
   uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
@@ -314,21 +312,20 @@
   let val [xT] = Term.rename_wrt_term t [(x, T)]
   in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
 
-fun abs_ast_tr' (*"_abs"*) asts =
+fun abs_ast_tr' asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
 
-fun preserve_binder_abs_tr' name syn = (name, fn (Abs abs :: ts) =>
-  let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ t, ts) end);
-
-fun preserve_binder_abs2_tr' name syn = (name, fn (A :: Abs abs :: ts) =>
-  let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+fun const_abs_tr' t =
+  (case eta_abs t of
+    Abs (_, _, t') =>
+      if Term.is_dependent t' then raise Match
+      else incr_boundvars ~1 t'
+  | _ => raise Match);
 
 
-(* binder *)
+(* binders *)
 
 fun mk_binder_tr' (name, syn) =
   let
@@ -345,6 +342,14 @@
       | binder_tr' [] = raise Match;
   in (name, binder_tr') end;
 
+fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ t, ts) end);
+
+fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+
 
 (* idtyp constraints *)
 
@@ -431,10 +436,10 @@
 val variant_abs' = var_abs mark_boundT;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
-      if Term.loose_bvar1 (B, 0) then
+      if Term.is_dependent B then
         let val (x', B') = variant_abs' (x, dummyT, B);
         in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
-      else Term.list_comb (Lexicon.const r $ A $ B, ts)
+      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;
 
 
@@ -443,8 +448,8 @@
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
-      if u aconv Bound i then Lexicon.const name $ tr' i t
-      else tr' i t $ tr' i u
+          if u aconv Bound i then Lexicon.const name $ tr' i t
+          else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
       | tr' i a = if a aconv Bound i then raise Match else a;
   in tr' 0 end;
@@ -461,16 +466,25 @@
 
 (* corresponding updates *)
 
+local
+
+fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
+  | upd_type _ = dummyT;
+
 fun upd_tr' (x_upd, T) =
   (case try (unsuffix "_update") x_upd of
-    SOME x => (x, if T = dummyT then T else Term.domain_type T)
+    SOME x => (x, upd_type T)
   | NONE => raise Match);
 
+in
+
 fun update_name_tr' (Free x) = Free (upd_tr' x)
   | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
   | update_name_tr' (Const x) = Const (upd_tr' x)
   | update_name_tr' _ = raise Match;
 
+end;
+
 
 (* indexed syntax *)
 
diff -r bb8986475416 -r 524bb42442dc src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/consts.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -255,7 +255,7 @@
 local
 
 fun strip_abss (t as Abs (x, T, b)) =
-      if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T)
+      if Term.is_dependent b then strip_abss b |>> cons (x, T)  (* FIXME decr!? *)
       else ([], t)
   | strip_abss t = ([], t);
 
diff -r bb8986475416 -r 524bb42442dc src/Pure/envir.ML
--- a/src/Pure/envir.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/envir.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -255,12 +255,12 @@
 fun eta (Abs (a, T, body)) =
     ((case eta body of
         body' as (f $ Bound 0) =>
-          if loose_bvar1 (f, 0) then Abs (a, T, body')
+          if Term.is_dependent f then Abs (a, T, body')
           else decrh 0 f
      | body' => Abs (a, T, body')) handle Same.SAME =>
         (case body of
           f $ Bound 0 =>
-            if loose_bvar1 (f, 0) then raise Same.SAME
+            if Term.is_dependent f then raise Same.SAME
             else decrh 0 f
         | _ => raise Same.SAME))
   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
diff -r bb8986475416 -r 524bb42442dc src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/pattern.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -316,7 +316,7 @@
   let
     fun mtch k (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
-          if k > 0 andalso loose_bvar(t,0) then raise MATCH
+          if k > 0 andalso Term.is_open t then raise MATCH
           else (case Envir.lookup' (insts, (ixn, T)) of
                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
                            Vartab.update_new (ixn, (T, t)) insts)
diff -r bb8986475416 -r 524bb42442dc src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/term.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -154,6 +154,8 @@
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
+  val is_open: term -> bool
+  val is_dependent: term -> bool
   val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
@@ -650,6 +652,9 @@
   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   | loose_bvar1 _ = false;
 
+fun is_open t = loose_bvar (t, 0);
+fun is_dependent t = loose_bvar1 (t, 0);
+
 (*Substitute arguments for loose bound variables.
   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
diff -r bb8986475416 -r 524bb42442dc src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Tools/atomize_elim.ML	Sat Mar 26 15:55:22 2011 +0100
@@ -80,7 +80,7 @@
       fun movea_conv ctxt ct =
           let
             val _ $ Abs (_, _, b) = term_of ct
-            val idxs = fold_index (fn (i, t) => not (loose_bvar1 (t, 0)) ? cons i)
+            val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
                        (Logic.strip_imp_prems b) []
                        |> rev