# HG changeset patch
# User wenzelm
# Date 1634318731 -7200
# Node ID c960bfcb91db9384ec10323b2ba7a3124b035650
# Parent  8ee3d5d3c1bf14e34448c2a3a4ff97a783cd8b74
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Simplifier and equational conversions demand a proper proof context;

diff -r 8ee3d5d3c1bf -r c960bfcb91db NEWS
--- a/NEWS	Fri Oct 15 17:45:47 2021 +0200
+++ b/NEWS	Fri Oct 15 19:25:31 2021 +0200
@@ -287,6 +287,38 @@
 
 *** ML ***
 
+* Term operations under abstractions are now more robust (and more
+strict) by using the formal proof context in subsequent operations:
+
+  Variable.dest_abs
+  Variable.dest_abs_cterm
+  Variable.dest_all
+  Variable.dest_all_cterm
+
+This works under the assumption that terms are always properly declared
+to the proof context (e.g. via Variable.declare_term). Failure to do so,
+or working with the wrong context, will cause an error (exception Fail,
+based on Term.USED_FREE from Term.dest_abs_fresh).
+
+The Simplifier and equational conversions now use the above operations
+routinely, and thus require user-space tools to be serious about the
+proof context (notably in their use of Goal.prove, SUBPROOF etc.).
+INCOMPATIBILITY in add-on tools is to be expected occasionally: a proper
+context discipline needs to be followed.
+
+* Former operations Term.dest_abs and Logic.dest_all (without a proper
+context) have been discontinued. INCOMPATIBILITY, either use
+Variable.dest_abs etc. above, or the following operations that imitate
+the old behavior to a great extent:
+
+  Term.dest_abs_global
+  Logic.dest_all_global
+
+This works under the assumption that the given (sub-)term directly shows
+all free variables that need to be avoided when generating a fresh name.
+A violation of the assumption are variables stemming from the enclosing
+context that get involved in a proof only later.
+
 * ML structures TFrees, TVars, Frees, Vars, Names provide scalable
 operations to accumulate items from types and terms, using a fast
 syntactic order. The original order of occurrences may be recovered as
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/FOLP/simp.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -366,7 +366,7 @@
 (*Replace parameters by Free variables in P*)
 fun variants_abs ([],P) = P
   | variants_abs ((a,T)::aTs, P) =
-      variants_abs (aTs, #2 (Term.dest_abs(a,T,P)));
+      variants_abs (aTs, #2 (Term.dest_abs_global (Abs (a,T,P))));
 
 (*Select subgoal i from proof state; substitute parameters, for printing*)
 fun prepare_goal i st =
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -92,7 +92,7 @@
           app_union_ct_pair find (Thm.dest_comb ct)
         | Abs (_, _, _) =>
           (* ensure the point doesn't contain the bound variable *)
-          let val (var, bod) = Thm.dest_abs ct in
+          let val (var, bod) = Thm.dest_abs_global ct in
             filter (free_in var #> not) (find bod)
           end
         | _ => [])
@@ -120,7 +120,7 @@
       | _ $ _ =>
         app_union_ct_pair find (Thm.dest_comb ct)
       | Abs (_, _, _) =>
-        let val (var, bod) = Thm.dest_abs ct in
+        let val (var, bod) = Thm.dest_abs_global ct in
           filter (free_in var #> not) (find bod)
         end
       | _ => []
@@ -139,7 +139,7 @@
           else app_union_ct_pair find (Thm.dest_binop ct)
       | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
       | Abs (_, _, _) =>
-        let val (var, bod) = Thm.dest_abs ct in
+        let val (var, bod) = Thm.dest_abs_global ct in
           filter (free_in var #> not) (find bod)
         end
       | _ => []
@@ -255,7 +255,7 @@
       let val (s, t) = Thm.dest_comb ct in
         default (find_dist t) (find_dist s)
       end
-    | Abs (_, _, _) => find_dist (snd (Thm.dest_abs ct))
+    | Abs (_, _, _) => find_dist (snd (Thm.dest_abs_global ct))
     | _ => NONE
   fun find_eq ct =
     case Thm.term_of ct of
@@ -269,7 +269,7 @@
       let val (s, t) = Thm.dest_comb ct in
         default (find_eq t) (find_eq s)
       end
-    | Abs (_, _, _) => find_eq (snd (Thm.dest_abs ct))
+    | Abs (_, _, _) => find_eq (snd (Thm.dest_abs_global ct))
     | _ => NONE
   in
     case default (find_eq ct) (find_dist ct) of
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 15 19:25:31 2021 +0200
@@ -2427,15 +2427,15 @@
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs \<^Const_>\<open>HOL.Not for t'\<close> =
       @{code Not} (fm_of_term ps vs t')
-  | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
+  | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>t as Abs (_, _, p)\<close>\<close> =
       let
-        val (xn', p') = Term.dest_abs (xn, xT, p);
-        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+        val (x', p') = Term.dest_abs_global t;
+        val vs' = (Free x', 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code E} (fm_of_term ps vs' p) end
-  | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
+  | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>t as Abs (_, _, p)\<close>\<close> =
       let
-        val (xn', p') = Term.dest_abs (xn, xT, p);
-        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+        val (x', p') = Term.dest_abs_global t;
+        val vs' = (Free x', 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code A} (fm_of_term ps vs' p) end
   | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
 
@@ -2505,7 +2505,7 @@
     | f $ a =>
         if is_ty t orelse is_op t then term_bools (term_bools acc f) a
         else insert (op aconv) t acc
-    | Abs p => term_bools acc (snd (Term.dest_abs p))
+    | Abs _ => term_bools acc (snd (Term.dest_abs_global t))
     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
   end;
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 15 19:25:31 2021 +0200
@@ -3974,12 +3974,12 @@
       @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
   | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> =
       @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
-  | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) =
-      let val (xn', p') = Term.dest_abs abs
-      in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
-  | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) =
-      let val (xn', p') = Term.dest_abs abs
-      in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
+  | fm_of_term fs ps \<^Const_>\<open>Ex _ for \<open>p as Abs _\<close>\<close> =
+      let val (x', p') = Term.dest_abs_global p
+      in @{code E} (fm_of_term (Free x' :: fs) ps p') end
+  | fm_of_term fs ps \<^Const_>\<open>All _ for \<open>p as Abs _\<close>\<close> =
+      let val (x', p') = Term.dest_abs_global p
+      in @{code A} (fm_of_term (Free x' :: fs) ps p') end
   | fm_of_term fs ps _ = error "fm_of_term";
 
 fun term_of_num T ps (@{code poly.C} (a, b)) =
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -24,7 +24,7 @@
                  simpset : simpset};
 
 fun get_p1 th =
-  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
+  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs_global)
     (funpow 2 Thm.dest_arg (Thm.cprop_of th)) |> Thm.dest_arg
 
 fun ferrack_conv ctxt
@@ -55,7 +55,7 @@
     in (S,th) end
 
  val ((p1_v,p2_v),(mp1_v,mp2_v)) =
-   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
+   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs_global)
      (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
    |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
    |> apply2 (apply2 (dest_Var o Thm.term_of))
@@ -78,8 +78,8 @@
  fun main vs p =
   let
    val ((xn,ce),(x,fm)) = (case Thm.term_of p of
-                   \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> =>
-                        Thm.dest_comb p ||> Thm.dest_abs_name xn |>> pair xn
+                   \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
+                        Thm.dest_comb p ||> Thm.dest_abs_global |>> pair xn
                  | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    val cT = Thm.ctyp_of_cterm x
    val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
@@ -174,25 +174,25 @@
 
 val grab_atom_bop =
  let
-  fun h bounds tm =
+  fun h ctxt tm =
    (case Thm.term_of tm of
-     \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
-   | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-   | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-   | \<^Const_>\<open>conj for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>disj for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>implies for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
-   | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-   | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
+     \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>Not for _\<close> => h ctxt (Thm.dest_arg tm)
+   | \<^Const_>\<open>All _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+   | \<^Const_>\<open>Ex _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+   | \<^Const_>\<open>conj for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>disj for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>implies for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args ctxt tm
+   | \<^Const_>\<open>Pure.all _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+   | \<^Const_>\<open>Trueprop for _\<close> => h ctxt (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
-  and find_args bounds tm =
-           (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
- and find_body bounds b =
-   let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
-   in h (bounds + 1) b' end;
+  and find_args ctxt tm =
+           (h ctxt (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
+ and find_body ctxt b =
+   let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+   in h ctxt' b' end;
 in h end;
 
 fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm =
@@ -213,7 +213,7 @@
  in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;
 
 fun dlo_instance ctxt tm =
-  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
+  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop ctxt tm);
 
 fun dlo_conv ctxt tm =
   (case dlo_instance ctxt tm of
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -41,7 +41,7 @@
           simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
             (Thm.instantiate' [] [SOME p] stupid)
         val (L, U) =
-          let val (_, q) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of ths))
+          let val (_, q) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of ths))
           in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
         fun proveneF S =
           let
@@ -128,10 +128,11 @@
 
 fun proc ctxt ct =
   (case Thm.term_of ct of
-    \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
+    \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
       let
         val e = Thm.dest_fun ct
-        val (x,p) = Thm.dest_abs_name xn (Thm.dest_arg ct)
+        val (x,p) = Thm.dest_abs_global (Thm.dest_arg ct)
+        val Free (xn, _) = Thm.term_of x
         val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p
         val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
       in
@@ -193,29 +194,29 @@
 
 val grab_atom_bop =
   let
-    fun h bounds tm =
+    fun h ctxt tm =
       (case Thm.term_of tm of
-        \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
-      | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-      | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-      | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
-      | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
-      | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
+        \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>Not for _\<close> => h ctxt (Thm.dest_arg tm)
+      | \<^Const_>\<open>All _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+      | \<^Const_>\<open>Pure.all _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+      | \<^Const_>\<open>Ex _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
+      | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args ctxt tm
+      | \<^Const_>\<open>Trueprop for _\<close> => h ctxt (Thm.dest_arg tm)
       | _ => Thm.dest_fun2 tm)
-    and find_args bounds tm =
-      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
-    and find_body bounds b =
-      let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
-      in h (bounds + 1) b' end;
+    and find_args ctxt tm =
+      (h ctxt (Thm.dest_arg tm) handle CTERM _ => h ctxt (Thm.dest_arg1 tm))
+    and find_body ctxt b =
+      let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+      in h ctxt' b' end;
   in h end;
 
 fun dlo_instance ctxt tm =
-  (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
+  (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop ctxt tm));
 
 fun dlo_conv ctxt tm =
   (case dlo_instance ctxt tm of
@@ -240,7 +241,7 @@
           then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
           else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
       | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-      | Abs _ => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
+      | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc))
       | Free _ => if member (op aconvc) ats t then acc else ins t acc
       | Var _ => if member (op aconvc) ats t then acc else ins t acc
       | _ => acc)
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -251,7 +251,7 @@
                     ^ ML_Syntax.print_term pat)
 
 fun strip_alls t =
-  (case try Logic.dest_all t of
+  (case try Logic.dest_all_global t of
     SOME (_, u) => strip_alls u
   | NONE => t)
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Fri Oct 15 19:25:31 2021 +0200
@@ -55,7 +55,7 @@
 fun as_typ a = a --> a --> a
 
 fun strip_all t =
-  case try Logic.dest_all t of
+  case try Logic.dest_all_global t of
     NONE => ([], t)
   | SOME (var, t) => apfst (cons var) (strip_all t)
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -308,7 +308,7 @@
   if p t then t else
   case Thm.term_of t of
     _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
-  | Abs (_,_,_) => find_cterm p (Thm.dest_abs t |> snd)
+  | Abs (_,_,_) => find_cterm p (Thm.dest_abs_global t |> snd)
   | _ => raise CTERM ("find_cterm",[t]);
 
 fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
@@ -496,7 +496,7 @@
         fun h (acc, t) =
           case Thm.term_of t of
             Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
-              h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+              h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
       end
@@ -541,7 +541,7 @@
         fun h (acc, t) =
           case Thm.term_of t of
             Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
-              h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+              h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
       end
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/cconv.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -152,8 +152,7 @@
            end
 
          (* Destruct the abstraction and apply the conversion. *)
-         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
-         val (v, ct') = Thm.dest_abs_name u ct
+         val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt
          val eq = cv (v, ctxt') ct'
        in
          if Thm.is_reflexive eq
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -774,7 +774,7 @@
 fun dest_comb t = Thm.dest_comb t
   handle CTERM (msg, _) => raise ERR "dest_comb" msg;
 
-fun dest_abs t = Thm.dest_abs t
+fun dest_abs t = Thm.dest_abs_global t
   handle CTERM (msg, _) => raise ERR "dest_abs" msg;
 
 fun capply t u = Thm.apply t u
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Real_Asymp/exp_log_expression.ML
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -164,8 +164,7 @@
         handle Pattern.MATCH => NONE
     fun rewrite_subterm prems ct (Abs (x, _, _)) =
       let
-        val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt;
-        val (v, ct') = Thm.dest_abs_name u ct;
+        val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
         val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct'
       in
         if Thm.is_reflexive thm then
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -321,7 +321,7 @@
 fun strip_top_all_vars acc t =
   if Logic.is_all t then
     let
-      val (v, t') = Logic.dest_all t
+      val (v, t') = Logic.dest_all_global t
       (*bound instances in t' are replaced with free vars*)
     in
       strip_top_all_vars (v :: acc) t'
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -451,9 +451,9 @@
           make_case ctxt (if b = \<^term>\<open>True\<close> then Error else Warning)
             Name.context (decode_case u) (decode_cases t)
       | decode_case (t $ u) = decode_case t $ decode_case u
-      | decode_case (Abs (x, T, u)) =
-          let val (x', u') = Term.dest_abs (x, T, u);
-          in Term.absfree (x', T) (decode_case u') end
+      | decode_case (t as Abs _) =
+          let val (v, t') = Term.dest_abs_global t;
+          in Term.absfree v (decode_case t') end
       | decode_case t = t;
   in
     map decode_case
@@ -587,9 +587,9 @@
   | NONE =>
       (case t of
         t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u
-      | Abs (x, T, u) =>
-          let val (x', u') = Term.dest_abs (x, T, u);
-          in Term.absfree (x', T) (strip_case_full ctxt d u') end
+      | Abs _ =>
+          let val (v, t') = Term.dest_abs_global t;
+          in Term.absfree v (strip_case_full ctxt d t') end
       | _ => t));
 
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -50,9 +50,9 @@
 
 
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
-fun dest_all_all (t as (Const (\<^const_name>\<open>Pure.all\<close>,_) $ _)) =
+fun dest_all_all \<^Const>\<open>Pure.all _ for t\<close> =
   let
-    val (v,b) = Logic.dest_all t |> apfst Free
+    val (v,b) = Term.dest_abs_global t |>> Free
     val (vs, b') = dest_all_all b
   in
     (v :: vs, b')
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -71,7 +71,7 @@
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
-      | dec_sko \<^Const_>\<open>All _ for \<open>Abs abs\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs abs)) rhss
+      | dec_sko \<^Const_>\<open>All _ for \<open>t as Abs _\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs_global t)) rhss
       | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
@@ -90,7 +90,7 @@
 fun abstract ctxt ct =
   let
       val Abs (_, _, body) = Thm.term_of ct
-      val (x, cbody) = Thm.dest_abs ct
+      val (x, cbody) = Thm.dest_abs_global ct
       val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
       fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
   in
@@ -142,7 +142,7 @@
   else case Thm.term_of ct of
     Abs _ =>
     let
-      val (cv, cta) = Thm.dest_abs ct
+      val (cv, cta) = Thm.dest_abs_global ct
       val (v, _) = dest_Free (Thm.term_of cv)
       val u_th = introduce_combinators_in_cterm ctxt cta
       val cu = Thm.rhs_of u_th
@@ -174,7 +174,7 @@
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
 fun c_variant_abs_multi (ct0, vars) =
-      let val (cv,ct) = Thm.dest_abs ct0
+      let val (cv,ct) = Thm.dest_abs_global ct0
       in  c_variant_abs_multi (ct, cv::vars)  end
       handle CTERM _ => (ct0, rev vars);
 
@@ -263,10 +263,10 @@
 fun zap pos ct =
   ct
   |> (case Thm.term_of ct of
-        Const (s, _) $ Abs (s', _, _) =>
+        Const (s, _) $ Abs _ =>
         if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
            s = \<^const_name>\<open>Ex\<close> then
-          Thm.dest_comb #> snd #> Thm.dest_abs_name s' #> snd #> zap pos
+          Thm.dest_comb #> snd #> Thm.dest_abs_global #> snd #> zap pos
         else
           Conv.all_conv
       | Const (s, _) $ _ $ _ =>
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -145,7 +145,7 @@
 
 fun get_pmi_term t =
   let val (x,eq) =
-     (Thm.dest_abs o Thm.dest_arg o snd o Thm.dest_abs o Thm.dest_arg)
+     (Thm.dest_abs_global o Thm.dest_arg o snd o Thm.dest_abs_global o Thm.dest_arg)
         (Thm.dest_arg t)
 in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
 
@@ -348,7 +348,7 @@
 
 fun unify ctxt q =
  let
-  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs
+  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs_global
   val x = Thm.term_of cx
   val ins = insert (op = : int * int -> bool)
   fun h (acc,dacc) t =
@@ -436,8 +436,8 @@
 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
 val [A_v,B_v] =
   map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
-    |> Thm.dest_abs |> snd |> Thm.dest_arg1 |> Thm.dest_arg
-    |> Thm.dest_abs |> snd |> Thm.dest_fun |> Thm.dest_arg
+    |> Thm.dest_abs_global |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+    |> Thm.dest_abs_global |> snd |> Thm.dest_fun |> Thm.dest_arg
     |> Thm.term_of |> dest_Var) [asetP, bsetP];
 
 val D_v = (("D", 0), \<^typ>\<open>int\<close>);
@@ -446,7 +446,7 @@
 let
 
  val uth = unify ctxt q
- val (x,p) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of uth))
+ val (x,p) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of uth))
  val ins = insert (op aconvc)
  fun h t (bacc,aacc,dacc) =
   case (whatis x t) of
@@ -599,12 +599,12 @@
               else insert (op aconv) t
     | f $ a => if skip orelse is_op f then add_bools a o add_bools f
               else insert (op aconv) t
-    | Abs p => add_bools (snd (Term.dest_abs p))
+    | Abs _ => add_bools (snd (Term.dest_abs_global t))
     | _ => if skip orelse is_op t then I else insert (op aconv) t
   end;
 
 fun descend vs (abs as (_, xT, _)) =
-  let val (xn', p') = Term.dest_abs abs
+  let val ((xn', _), p') = Term.dest_abs_global (Abs abs)
   in ((xn', xT) :: vs, p') end;
 
 local structure Proc = Cooper_Procedure in
@@ -716,8 +716,8 @@
 
 fun strip_objall ct =
  case Thm.term_of ct of
-  Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) =>
-   let val (a,(v,t')) = (apsnd (Thm.dest_abs_name xn) o Thm.dest_comb) ct
+  Const (\<^const_name>\<open>All\<close>, _) $ Abs _ =>
+   let val (a,(v,t')) = (apsnd Thm.dest_abs_global o Thm.dest_comb) ct
    in apfst (cons (a,v)) (strip_objall t')
    end
 | _ => ([],ct);
@@ -798,7 +798,7 @@
   fun h acc t = if ty cts t then insert (op aconvc) t acc else
    case Thm.term_of t of
     _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
+  | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc))
   | _ => acc
  in h [] ct end
 end;
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -29,10 +29,10 @@
        then Conv.binop_conv (conv env) p
        else atcv env p
   | Const(\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv (conv env) p
-  | Const(\<^const_name>\<open>Ex\<close>,_)$Abs(s,_,_) =>
+  | Const(\<^const_name>\<open>Ex\<close>,_)$Abs (s, _, _) =>
     let
      val (e,p0) = Thm.dest_comb p
-     val (x,p') = Thm.dest_abs_name s p0
+     val (x,p') = Thm.dest_abs_global p0
      val env' = ins x env
      val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
                    |> Drule.arg_cong_rule e
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -221,7 +221,7 @@
 
 fun unlam t =
   (case t of
-    Abs a => snd (Term.dest_abs a)
+    Abs _ => snd (Term.dest_abs_global t)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
 
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -713,12 +713,12 @@
         mk_repabs ctxt (rty, qty) (Const (\<^const_name>\<open>Babs\<close>, T) $ r $ (inj_repabs_trm ctxt (t, t')))
       end
 
-  | (Abs (x, T, t), Abs (x', T', t')) =>
+  | (t as Abs _, t' as Abs _) =>
       let
         val rty = fastype_of rtrm
         val qty = fastype_of qtrm
-        val (y, s) = Term.dest_abs (x, T, t)
-        val (_, s') = Term.dest_abs (x', T', t')
+        val ((y, T), s) = Term.dest_abs_global t
+        val (_, s') = Term.dest_abs_global t'
         val yvar = Free (y, T)
         val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
       in
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -382,7 +382,7 @@
         let val (cu1, cu2) = Thm.dest_comb ct
         in f vs cu1 cu2 #> add_apps f vs cu1 #> add_apps f vs cu2 end
     | Abs _ =>
-        let val (cv, cu) = Thm.dest_abs ct
+        let val (cv, cu) = Thm.dest_abs_global ct
         in add_apps f (Thm.term_of cv :: vs) cu end
     | _ => I)
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -181,12 +181,7 @@
 
 (* certified terms *)
 
-fun dest_cabs ct ctxt =
-  (case Thm.term_of ct of
-    Abs _ =>
-      let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
-      in (snd (Thm.dest_abs_name n ct), ctxt') end
-  | _ => raise CTERM ("no abstraction", [ct]))
+fun dest_cabs ct ctxt = Variable.dest_abs_cterm ct ctxt |>> #1
 
 val dest_all_cabs = repeat_yield (try o dest_cabs)
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -62,10 +62,9 @@
           end
       end
 
-fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (abs as (_, T, _))) =
-    let val (s', t') = Term.dest_abs abs in
-      dest_alls t' |>> cons (s', T)
-    end
+fun dest_alls \<^Const_>\<open>Pure.all _ for \<open>t as Abs _\<close>\<close> =
+    let val (v, t') = Term.dest_abs_global t
+    in dest_alls t' |>> cons v end
   | dest_alls t = ([], t)
 
 val reorder_foralls =
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -385,8 +385,8 @@
 val strip_exists =
  let fun h (acc, t) =
       case Thm.term_of t of
-       Const (\<^const_name>\<open>Ex\<close>, _) $ Abs _ =>
-        h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
+       \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
+        h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
      | _ => (acc,t)
  in fn t => h ([],t)
  end;
@@ -885,40 +885,40 @@
 end;
 
 
-fun find_term bounds tm =
+fun find_term tm ctxt =
   (case Thm.term_of tm of
     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
-      if domain_type T = HOLogic.boolT then find_args bounds tm
-      else Thm.dest_arg tm
-  | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term bounds (Thm.dest_arg tm)
-  | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-  | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
-  | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
-  | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
-  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
-  | Const("(==)",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
-  | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
+      if domain_type T = HOLogic.boolT then find_args tm ctxt
+      else (Thm.dest_arg tm, ctxt)
+  | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term (Thm.dest_arg tm) ctxt
+  | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
+  | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
+  | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args tm ctxt
+  | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args tm ctxt
+  | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args tm ctxt
+  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args tm ctxt
+  | Const("(==)",_)$_$_ => find_args tm ctxt  (* FIXME proper const name *)
+  | \<^term>\<open>Trueprop\<close>$_ => find_term (Thm.dest_arg tm) ctxt
   | _ => raise TERM ("find_term", []))
-and find_args bounds tm =
+and find_args tm ctxt =
   let val (t, u) = Thm.dest_binop tm
-  in (find_term bounds t handle TERM _ => find_term bounds u) end
-and find_body bounds b =
-  let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
-  in find_term (bounds + 1) b' end;
+  in (find_term t ctxt handle TERM _ => find_term u ctxt) end
+and find_body b ctxt =
+  let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
+  in find_term b' ctxt' end;
 
 
 fun get_ring_ideal_convs ctxt form =
- case try (find_term 0) form of
+ case \<^try>\<open>find_term form ctxt\<close> of
   NONE => NONE
-| SOME tm =>
-  (case Semiring_Normalizer.match ctxt tm of
+| SOME (tm, ctxt') =>
+  (case Semiring_Normalizer.match ctxt' tm of
     NONE => NONE
   | SOME (res as (theory, {is_const = _, dest_const,
           mk_const, conv = ring_eq_conv})) =>
      SOME (ring_and_ideal_conv theory
-          dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt)
-          (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
+          dest_const (mk_const (Thm.ctyp_of_cterm tm)) (ring_eq_conv ctxt')
+          (Semiring_Normalizer.semiring_normalize_wrapper ctxt' res)))
 
 fun presimplify ctxt add_thms del_thms =
   asm_full_simp_tac (put_simpset HOL_basic_ss ctxt
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/Tools/reification.ML
--- a/src/HOL/Tools/reification.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/reification.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -136,13 +136,10 @@
     val thy = Proof_Context.theory_of ctxt;
     fun tryabsdecomp (ct, ctxt) bds =
       (case Thm.term_of ct of
-        Abs (_, xT, ta) =>
+        Abs (_, xT, _) =>
           let
-            val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
-            val (xn, ta) = Term.dest_abs (raw_xn, xT, ta);
-            val x = Free (xn, xT);
-            val cx = Thm.cterm_of ctxt' x;
-            val cta = Thm.cterm_of ctxt' ta;
+            val ((cx, cta), ctxt') = Variable.dest_abs_cterm ct ctxt;
+            val x = Thm.term_of cx;
             val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
                 NONE => error "tryabsdecomp: Type not found in the Environement"
               | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Fri Oct 15 19:25:31 2021 +0200
@@ -12,7 +12,7 @@
 ML \<open>
 fun split_clause t =
   let
-    val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all t;
+    val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all_global t;
     val assms = Logic.strip_imp_prems horn;
     val concl = Logic.strip_imp_concl horn;
   in (fixes, assms, concl) end;
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -231,14 +231,17 @@
 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
 
 (* Does pat match a subterm of obj? *)
-fun matches_subterm thy (pat, obj) =
+fun matches_subterm ctxt (pat, obj) =
   let
-    fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
+    val thy = Proof_Context.theory_of ctxt;
+    fun matches obj ctxt' = Pattern.matches thy (pat, obj) orelse
       (case obj of
-        Abs (_, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
-      | t $ u => msub bounds t orelse msub bounds u
-      | _ => false)
-  in msub 0 obj end;
+        Abs (_, T, t) =>
+          let val ((_, t'), ctxt'') = Variable.dest_abs obj ctxt'
+          in matches t' ctxt'' end
+      | t $ u => matches t ctxt' orelse matches u ctxt'
+      | _ => false);
+  in matches obj ctxt end;
 
 (*Including all constants and frees is only sound because matching
   uses higher-order patterns. If full matching were used, then
@@ -255,7 +258,7 @@
     fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
       | check ((_, thm), c as SOME thm_consts) =
          (if subset (op =) (pat_consts, thm_consts) andalso
-            matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm)
+            matches_subterm ctxt (pat', Thm.full_prop_of thm)
           then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
   in check end;
 
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/conv.ML
--- a/src/Pure/conv.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/conv.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -91,12 +91,11 @@
 
 fun abs_conv cv ctxt ct =
   (case Thm.term_of ct of
-    Abs (x, _, _) =>
+    Abs (a, _, _) =>
       let
-        val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
-        val (v, ct') = Thm.dest_abs_name u ct;
+        val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
         val eq = cv (v, ctxt') ct';
-      in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
+      in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule a v eq end
   | _ => raise CTERM ("abs_conv", [ct]));
 
 fun combination_conv cv1 cv2 ct =
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/logic.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -11,7 +11,7 @@
   val all: term -> term -> term
   val dependent_all_name: string * term -> term -> term
   val is_all: term -> bool
-  val dest_all: term -> (string * typ) * term
+  val dest_all_global: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
   val all_constraint: (string -> typ option) -> string * string -> term -> term
   val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
@@ -125,10 +125,10 @@
 fun is_all (Const ("Pure.all", _) $ Abs _) = true
   | is_all _ = false;
 
-fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
-      let val (x, b) = Term.dest_abs abs  (*potentially slow*)
-      in ((x, T), b) end
-  | dest_all t = raise TERM ("dest_all", [t]);
+fun dest_all_global t =
+  (case t of
+    Const ("Pure.all", _) $ (u as Abs _) => Term.dest_abs_global u
+  | _ => raise TERM ("dest_all", [t]));
 
 fun list_all ([], t) = t
   | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/more_pattern.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -48,9 +48,11 @@
   let
     val skel0 = Bound 0;
 
-    fun variant_absfree bounds (x, T, t) =
+    fun variant_absfree bounds x tm =
       let
-        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
+        val ((x', T), t') =
+          Term.dest_abs_fresh (Name.bound bounds) tm
+            handle Term.USED_FREE _ => Term.dest_abs_global tm;  (* FIXME proper context *)
         fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
       in (abs, t') end;
 
@@ -76,9 +78,9 @@
                     SOME tm2' => SOME (tm1 $ tm2')
                   | NONE => NONE)
             end)
-      | rew_sub r bounds skel (Abs body) =
+      | rew_sub r bounds skel (tm as Abs (x, _, _)) =
           let
-            val (abs, tm') = variant_absfree bounds body;
+            val (abs, tm') = variant_absfree bounds x tm;
             val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
           in case r (bounds + 1) skel' tm' of
               SOME tm'' => SOME (abs tm'')
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -336,36 +336,48 @@
 
 local
 
-fun dest_all ct =
+val used_frees =
+  Name.build_context o
+    Thm.fold_terms {hyps = true} Term.declare_term_frees;
+
+fun used_vars i =
+  Name.build_context o
+    (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+      (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I);
+
+fun dest_all ct used =
   (case Thm.term_of ct of
-    Const ("Pure.all", _) $ Abs (a, _, _) =>
-      let val (x, ct') = Thm.dest_abs (Thm.dest_arg ct)
-      in SOME ((a, Thm.ctyp_of_cterm x), ct') end
+    Const ("Pure.all", _) $ Abs (x, _, _) =>
+      let
+        val (x', used') = Name.variant x used;
+        val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct);
+      in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end
   | _ => NONE);
 
-fun dest_all_list ct =
-  (case dest_all ct of
-    NONE => []
-  | SOME (v, ct') => v :: dest_all_list ct');
+fun dest_all_list ct used =
+  (case dest_all ct used of
+    NONE => ([], used)
+  | SOME (v, (ct', used')) =>
+      let val (vs, used'') = dest_all_list ct' used'
+      in (v :: vs, used'') end);
 
 fun forall_elim_vars_list vars i th =
   let
-    val used =
-      (Thm.fold_terms {hyps = false} o Term.fold_aterms)
-        (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
-    val vars' = (Name.variant_list used (map #1 vars), vars)
-      |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
+    val (vars', _) =
+      (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used =>
+        let val (x', used') = Name.variant x used
+        in (Thm.var ((x', i), T), used') end);
   in fold Thm.forall_elim vars' th end;
 
 in
 
 fun forall_elim_vars i th =
-  forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th;
+  forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th;
 
 fun forall_elim_var i th =
   let
     val vars =
-      (case dest_all (Thm.cprop_of th) of
+      (case dest_all (Thm.cprop_of th) (used_frees th) of
         SOME (v, _) => [v]
       | NONE => raise THM ("forall_elim_var", i, [th]));
   in forall_elim_vars_list vars i th end;
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -1130,21 +1130,13 @@
     and subc skel ctxt t0 =
         let val Simpset (_, {congs, ...}) = simpset_of ctxt in
           (case Thm.term_of t0 of
-              Abs (a, T, _) =>
+              Abs (a, _, _) =>
                 let
-                    val (v, ctxt') = Variable.next_bound (a, T) ctxt;
-                    val b = #1 (Term.dest_Free v);
-                    val (v', t') = Thm.dest_abs_name b t0;
-                    val b' = #1 (Term.dest_Free (Thm.term_of v'));
-                    val _ =
-                      if b <> b' then
-                        warning ("Bad Simplifier context: renamed bound variable " ^
-                          quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
-                      else ();
-                    val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
+                  val ((v, t'), ctxt') = Variable.dest_abs_cterm t0 ctxt;
+                  val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
                 in
                   (case botc skel' ctxt' t' of
-                    SOME thm => SOME (Thm.abstract_rule a v' thm)
+                    SOME thm => SOME (Thm.abstract_rule a v thm)
                   | NONE => NONE)
                 end
             | t $ _ =>
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/term.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -166,7 +166,9 @@
   val could_eta_contract: term -> bool
   val could_beta_eta_contract: term -> bool
   val used_free: string -> term -> bool
-  val dest_abs: string * typ * term -> string * term
+  exception USED_FREE of string * term
+  val dest_abs_fresh: string -> term -> (string * typ) * term
+  val dest_abs_global: term -> (string * typ) * term
   val dummy_pattern: typ -> term
   val dummy: term
   val dummy_prop: term
@@ -965,6 +967,9 @@
 
 (* dest abstraction *)
 
+(*ASSUMPTION: x is fresh wrt. the current context, but the check
+  of used_free merely guards against gross mistakes*)
+
 fun used_free x =
   let
     fun used (Free (y, _)) = (x = y)
@@ -973,11 +978,27 @@
       | used _ = false;
   in used end;
 
-fun dest_abs (x, T, b) =
-  if used_free x b then
-    let val (x', _) = Name.variant x (declare_term_frees b Name.context);
-    in (x', subst_bound (Free (x', T), b)) end
-  else (x, subst_bound (Free (x, T), b));
+exception USED_FREE of string * term;
+
+fun subst_abs v b = (v, subst_bound (Free v, b));
+
+fun dest_abs_fresh x t =
+  (case t of
+    Abs (_, T, b) =>
+      if used_free x b then raise USED_FREE (x, t)
+      else subst_abs (x, T) b
+  | _ => raise TERM ("dest_abs", [t]));
+
+fun dest_abs_global t =
+  (case t of
+    Abs (x, T, b) =>
+      if used_free x b then
+        let
+          val used = Name.build_context (declare_term_frees b);
+          val x' = #1 (Name.variant x used);
+        in subst_abs (x', T) b end
+      else subst_abs (x, T) b
+  | _ => raise TERM ("dest_abs", [t]));
 
 
 (* dummy patterns *)
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/thm.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -48,8 +48,8 @@
   val dest_arg: cterm -> cterm
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
-  val dest_abs_name: string -> cterm -> cterm * cterm
-  val dest_abs: cterm -> cterm * cterm
+  val dest_abs_fresh: string -> cterm -> cterm * cterm
+  val dest_abs_global: cterm -> cterm * cterm
   val rename_tvar: indexname -> ctyp -> ctyp
   val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
@@ -305,15 +305,18 @@
       in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
 
-fun dest_abs_name x (Cterm {t = Abs (_, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
-      let val (y', t') = Term.dest_abs (x, T, t) in
-        (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts},
-          Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts})
-      end
-  | dest_abs_name _ ct = raise CTERM ("dest_abs_name", [ct]);
+fun gen_dest_abs dest ct =
+  (case ct of
+    Cterm {t = t as Abs _, T = Type ("fun", [_, U]), cert, maxidx, sorts} =>
+      let
+        val ((x', T), t') = dest t;
+        val v = Cterm {t = Free (x', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts};
+        val body = Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts};
+      in (v, body) end
+  | _ => raise CTERM ("dest_abs", [ct]));
 
-fun dest_abs (ct as Cterm {t = Abs (x, _, _), ...}) = dest_abs_name x ct
-  | dest_abs ct = raise CTERM ("dest_abs", [ct]);
+val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh;
+val dest_abs_global = gen_dest_abs Term.dest_abs_global;
 
 
 (* constructors *)
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/variable.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -81,6 +81,10 @@
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
+  val dest_abs: term -> Proof.context -> ((string * typ) * term) * Proof.context
+  val dest_abs_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
+  val dest_all: term -> Proof.context -> ((string * typ) * term) * Proof.context
+  val dest_all_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
   val is_bound_focus: Proof.context -> bool
   val set_bound_focus: bool -> Proof.context -> Proof.context
   val restore_bound_focus: Proof.context -> Proof.context -> Proof.context
@@ -650,6 +654,40 @@
 val trade = gen_trade (import true) export;
 
 
+(* destruct binders *)
+
+local
+
+fun gen_dest_abs exn dest term_of arg ctxt =
+  (case term_of arg of
+    Abs (a, T, _) =>
+      let
+        val (x, ctxt') = yield_singleton bound_fixes (a, T) ctxt;
+        val res = dest x arg handle Term.USED_FREE _ =>
+          raise Fail ("Bad context: clash of fresh free for bound: " ^
+            Syntax.string_of_term ctxt (Free (x, T)) ^ " vs. " ^
+            Syntax.string_of_term ctxt' (Free (x, T)));
+      in (res, ctxt') end
+  | _ => raise exn ("dest_abs", [arg]));
+
+in
+
+val dest_abs = gen_dest_abs TERM Term.dest_abs_fresh I;
+val dest_abs_cterm = gen_dest_abs CTERM Thm.dest_abs_fresh Thm.term_of;
+
+fun dest_all t ctxt =
+  (case t of
+    Const ("Pure.all", _) $ u => dest_abs u ctxt
+  | _ => raise TERM ("dest_all", [t]));
+
+fun dest_all_cterm ct ctxt =
+  (case Thm.term_of ct of
+    Const ("Pure.all", _) $ _ => dest_abs_cterm (Thm.dest_arg ct) ctxt
+  | _ => raise CTERM ("dest_all", [ct]));
+
+end;
+
+
 (* focus on outermost parameters: \<And>x y z. B *)
 
 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -622,7 +622,7 @@
       pair (IVar (SOME v))
   | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
+        val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t));
         val v'' = if Term.used_free v' t' then SOME v' else NONE
       in
         translate_typ ctxt algbr eqngr permissive ty
diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -126,9 +126,9 @@
     it replaces the bound variables by free variables.  *)
 fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) =
       strip_context_aux (params, H :: Hs, B)
-  | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) =
-      let val (b, u) = Term.dest_abs (a, T, t)
-      in strip_context_aux ((b, T) :: params, Hs, u) end
+  | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>t as Abs _\<close>\<close>) =
+      let val (v, u) = Term.dest_abs_global t
+      in strip_context_aux (v :: params, Hs, u) end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
 
 fun strip_context A = strip_context_aux ([], [], A);