merged
authorwenzelm
Mon, 18 Oct 2021 18:33:46 +0200
changeset 74928 2ff001a8c9f2
parent 74904 dc1a7c10565b (current diff)
parent 74927 c87b403b03eb (diff)
child 74929 f55c632a1fe8
child 74931 d592354c4a26
child 74933 9864ab4c20ce
merged
--- a/NEWS	Thu Oct 14 16:56:02 2021 +0200
+++ b/NEWS	Mon Oct 18 18:33:46 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
--- a/src/FOLP/simp.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/FOLP/simp.ML	Mon Oct 18 18:33:46 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 =
--- a/src/HOL/Analysis/metric_arith.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Mon Oct 18 18:33:46 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 NONE 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 NONE 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 NONE 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 NONE 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 NONE ct))
+    | Abs (_, _, _) => find_eq (snd (Thm.dest_abs_global ct))
     | _ => NONE
   in
     case default (find_eq ct) (find_dist ct) of
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Oct 18 18:33:46 2021 +0200
@@ -2427,16 +2427,16 @@
       @{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 _\<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;
-      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> =
+        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>t as Abs _\<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;
-      in @{code A} (fm_of_term ps vs' p) end
+        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);
 
 fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
@@ -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;
 
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Oct 18 18:33:46 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)) =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -24,7 +24,7 @@
                  simpset : simpset};
 
 fun get_p1 th =
-  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+  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 NONE)
+   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 (SOME 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 (SOME (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
--- a/src/HOL/Decision_Procs/langford.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Mon Oct 18 18:33:46 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 NONE (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 (SOME 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 (SOME (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 NONE 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)
--- a/src/HOL/HOL.thy	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/HOL.thy	Mon Oct 18 18:33:46 2021 +0200
@@ -2104,9 +2104,9 @@
 method_setup eval = \<open>
   let
     fun eval_tac ctxt =
-      let val conv = Code_Runtime.dynamic_holds_conv ctxt
+      let val conv = Code_Runtime.dynamic_holds_conv
       in
-        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
+        CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN'
         resolve_tac ctxt [TrueI]
       end
   in
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Oct 18 18:33:46 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)
 
--- a/src/HOL/Library/Pattern_Aliases.thy	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Mon Oct 18 18:33:46 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)
 
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Mon Oct 18 18:33:46 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 NONE 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 NONE (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 NONE (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
--- a/src/HOL/Library/cconv.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Library/cconv.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -124,41 +124,37 @@
      Abs (x, _, _) =>
        let
          (* Instantiate the rule properly and apply it to the eq theorem. *)
-         fun abstract_rule u v eq =
+         fun abstract_rule v eq =
            let
              (* Take a variable v and an equality theorem of form:
                   P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
                 And build a term of form:
                   \<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
-             fun mk_concl var eq =
+             fun mk_concl eq =
                let
-                 val certify = Thm.cterm_of ctxt
-                 fun abs term = (Term.lambda var term) $ var
-                 fun equals_cong f t =
-                   Logic.dest_equals t
-                   |> (fn (a, b) => (f a, f b))
-                   |> Logic.mk_equals
+                 fun abs t = lambda v t $ v
+                 fun equals_cong f = Logic.dest_equals #> apply2 f #> Logic.mk_equals
                in
                  Thm.concl_of eq
                  |> equals_cong abs
-                 |> Logic.all var |> certify
+                 |> Logic.all v
+                 |> Thm.cterm_of ctxt
                end
              val rule = abstract_rule_thm x
-             val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
+             val inst = Thm.match (hd (Drule.cprems_of rule), mk_concl eq)
+             val gen = (Names.empty, Names.make_set [#1 (dest_Free v)])
            in
-             (Drule.instantiate_normalize inst rule OF
-               [Drule.generalize (Names.empty, Names.make_set [u]) eq])
+             (Drule.instantiate_normalize inst rule OF [Drule.generalize gen eq])
              |> Drule.zero_var_indexes
            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 (SOME 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_cconv ct
-         else abstract_rule u v eq
+         else abstract_rule (Thm.term_of v) eq
        end
    | _ => raise CTERM ("abs_cconv", [ct]))
 
@@ -173,8 +169,7 @@
   then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
   else cv ctxt ct
 
-(* TODO: This code behaves not exactly like Conv.prems_cconv does.
-         Fix this! *)
+(* FIXME: This code behaves not exactly like Conv.prems_cconv does. *)
 (*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun prems_cconv 0 cv ct = cv ct
   | prems_cconv n cv ct =
--- a/src/HOL/Library/old_recdef.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -110,7 +110,7 @@
 signature DCTERM =
 sig
   val dest_comb: cterm -> cterm * cterm
-  val dest_abs: string option -> cterm -> cterm * cterm
+  val dest_abs: cterm -> cterm * cterm
   val capply: cterm -> cterm -> cterm
   val cabs: cterm -> cterm -> cterm
   val mk_conj: cterm * cterm -> cterm
@@ -191,7 +191,7 @@
     term * term list * thm * thm list -> thm -> thm * term list
   val RIGHT_ASSOC: Proof.context -> thm -> thm
 
-  val prove: Proof.context -> bool -> term * tactic -> thm
+  val prove: Proof.context -> bool -> term -> (Proof.context -> tactic) -> thm
 end;
 
 signature THRY =
@@ -221,7 +221,9 @@
   val mk_induction: Proof.context ->
     {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
   val postprocess: Proof.context -> bool ->
-    {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
+    {wf_tac: Proof.context -> tactic,
+     terminator: Proof.context -> tactic,
+     simplifier: Proof.context -> cterm -> thm} ->
     {rules: thm, induction: thm, TCs: term list list} ->
     {rules: thm, induction: thm, nested_tcs: thm list}
 end;
@@ -774,7 +776,7 @@
 fun dest_comb t = Thm.dest_comb t
   handle CTERM (msg, _) => raise ERR "dest_comb" msg;
 
-fun dest_abs a t = Thm.dest_abs a 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
@@ -838,7 +840,7 @@
  in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
 
 fun dest_binder expected tm =
-  dest_abs NONE (dest_monop expected tm)
+  dest_abs (dest_monop expected tm)
   handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
 
 
@@ -883,7 +885,7 @@
 
 val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
 val strip_imp    = rev2swap o strip dest_imp
-val strip_abs    = rev2swap o strip (dest_abs NONE)
+val strip_abs    = rev2swap o strip dest_abs
 val strip_forall = rev2swap o strip dest_forall
 val strip_exists = rev2swap o strip dest_exists
 
@@ -1232,7 +1234,9 @@
 fun SUBS ctxt thl =
   rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
 
-val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
+fun rew_conv ctxt ctm =
+  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+    (Variable.declare_term (Thm.term_of ctm) ctxt) ctm;
 
 fun simpl_conv ctxt thl ctm =
   HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm);
@@ -1590,13 +1594,13 @@
  end;
 
 
-fun prove ctxt strict (t, tac) =
+fun prove ctxt strict t tac =
   let
     val ctxt' = Proof_Context.augment t ctxt;
   in
     if strict
-    then Goal.prove ctxt' [] [] t (K tac)
-    else Goal.prove ctxt' [] [] t (K tac)
+    then Goal.prove ctxt' [] [] t (tac o #context)
+    else Goal.prove ctxt' [] [] t (tac o #context)
       handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
   end;
 
@@ -1688,14 +1692,6 @@
 
 val list_mk_type = Utils.end_itlist (curry (op -->));
 
-fun front_last [] = raise TFL_ERR "front_last" "empty list"
-  | front_last [x] = ([],x)
-  | front_last (h::t) =
-     let val (pref,x) = front_last t
-     in
-        (h::pref,x)
-     end;
-
 
 (*---------------------------------------------------------------------------
  * The next function is common to pattern-match translation and
@@ -2053,8 +2049,6 @@
 end;
 
 
-fun givens pats = map pat_of (filter given pats);
-
 fun post_definition ctxt meta_tflCongs (def, pats) =
  let val thy = Proof_Context.theory_of ctxt
      val tych = Thry.typecheck thy
@@ -2408,11 +2402,13 @@
    (*---------------------------------------------------------------------
     * Attempt to eliminate WF condition. It's the only assumption of rules
     *---------------------------------------------------------------------*)
-    val (rules1,induction1)  =
-       let val thm =
-        Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
-       in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
-       end handle Utils.ERR _ => (rules,induction);
+    val ((rules1, induction1), ctxt') =
+      let
+        val thm =
+          Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules)))) wf_tac
+        val ctxt' = Variable.declare_thm thm ctxt
+      in ((Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction), ctxt')
+      end handle Utils.ERR _ => ((rules, induction), ctxt);
 
    (*----------------------------------------------------------------------
     * The termination condition (tc) is simplified to |- tc = tc' (there
@@ -2425,15 +2421,15 @@
 
    fun simplify_tc tc (r,ind) =
        let val tc1 = tych tc
-           val _ = trace_cterm ctxt "TC before simplification: " tc1
-           val tc_eq = simplifier tc1
-           val _ = trace_thms ctxt "result: " [tc_eq]
+           val _ = trace_cterm ctxt' "TC before simplification: " tc1
+           val tc_eq = simplifier ctxt' tc1
+           val _ = trace_thms ctxt' "result: " [tc_eq]
        in
        elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
        handle Utils.ERR _ =>
         (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
-                  (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
-                           terminator)))
+                  (Rules.prove ctxt' strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)))
+                           terminator))
                  (r,ind)
          handle Utils.ERR _ =>
           (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
@@ -2454,14 +2450,14 @@
     *   3. return |- tc = tc'
     *---------------------------------------------------------------------*)
    fun simplify_nested_tc tc =
-      let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
+      let val tc_eq = simplifier ctxt' (tych (#2 (USyntax.strip_forall tc)))
       in
-      Rules.GEN_ALL ctxt
+      Rules.GEN_ALL ctxt'
        (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
         handle Utils.ERR _ =>
           (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
-                      (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
-                               terminator))
+                      (Rules.prove ctxt' strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)))
+                               terminator)
             handle Utils.ERR _ => tc_eq))
       end
 
@@ -2512,12 +2508,12 @@
  *--------------------------------------------------------------------------*)
 fun std_postprocessor ctxt strict wfs =
   Prim.postprocess ctxt strict
-   {wf_tac = REPEAT (ares_tac ctxt wfs 1),
-    terminator =
-      asm_simp_tac ctxt 1
-      THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
-        fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
-    simplifier = Rules.simpl_conv ctxt []};
+   {wf_tac = fn ctxt' => REPEAT (ares_tac ctxt' wfs 1),
+    terminator = fn ctxt' =>
+      asm_simp_tac ctxt' 1
+      THEN TRY (Arith_Data.arith_tac ctxt' 1 ORELSE
+        fast_force_tac (ctxt' addSDs @{thms not0_implies_Suc}) 1),
+    simplifier = fn ctxt' => Rules.simpl_conv ctxt' []};
 
 
 
@@ -2581,7 +2577,8 @@
               val simplified' = map (join_assums ctxt) simplified
               val dummy = (Prim.trace_thms ctxt "solved =" solved;
                            Prim.trace_thms ctxt "simplified' =" simplified')
-              val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
+              fun rewr th =
+                full_simplify (Variable.declare_thm th ctxt addsimps (solved @ simplified')) th;
               val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
               val induction' = rewr induction
               val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
@@ -2610,6 +2607,9 @@
 val spec'=
   Rule_Insts.read_instantiate \<^context> [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
 
+fun rulify_no_asm ctxt th =
+  Object_Logic.rulify_no_asm (Variable.declare_thm th ctxt) th;
+
 fun simplify_defn ctxt strict congs wfs pats def0 =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -2624,10 +2624,9 @@
        {f = f, R = R, rules = rules,
         full_pats_TCs = full_pats_TCs,
         TCs = TCs}
-    val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
-                      (Rules.CONJUNCTS rules)
+    val rules' = map (Drule.export_without_context o rulify_no_asm ctxt) (Rules.CONJUNCTS rules)
   in
-    {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
+    {induct = meta_outer ctxt (rulify_no_asm ctxt (induction RS spec')),
      rules = ListPair.zip(rules', rows),
      tcs = (termination_goals rules') @ tcs}
   end
@@ -2645,7 +2644,7 @@
     | solve_eq _ (_, [a], i) = [(a, i)]
     | solve_eq ctxt (th, splitths, i) =
       (writeln "Proving unsplit equation...";
-      [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
+      [((Drule.export_without_context o rulify_no_asm ctxt)
           (CaseSplit.splitto ctxt splitths th), i)])
       handle ERROR s =>
              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
--- a/src/HOL/Library/simps_case_conv.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -64,8 +64,7 @@
   let
     val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
     val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
-    fun dest_alls (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = dest_alls t
-      | dest_alls t = t
+    val dest_alls = Term.strip_qnt_body \<^const_name>\<open>All\<close>
   in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
   handle TERM _ => false
 
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -25,7 +25,7 @@
     (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
+  (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt));
 
 fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
 
@@ -131,10 +131,10 @@
   let
     val prop = Thm.prop_of th;
     fun prove t =
-      Goal.prove ctxt [] [] t (fn _ =>
-        EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
-          REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
-          REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
+      Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} =>
+        EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1,
+          REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)),
+          REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))])
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
 val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
@@ -146,23 +146,23 @@
 fun first_order_mrs ths th = ths MRS
   Thm.instantiate (first_order_matchs (cprems_of th) (map Thm.cprop_of ths)) th;
 
-fun prove_strong_ind s avoids ctxt =
+fun prove_strong_ind s avoids lthy =
   let
-    val thy = Proof_Context.theory_of ctxt;
+    val thy = Proof_Context.theory_of lthy;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global lthy (Sign.intern_const thy s);
     val ind_params = Inductive.params_of raw_induct;
-    val raw_induct = atomize_induct ctxt raw_induct;
-    val elims = map (atomize_induct ctxt) elims;
-    val monos = Inductive.get_monos ctxt;
-    val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
+    val raw_induct = atomize_induct lthy raw_induct;
+    val elims = map (atomize_induct lthy) elims;
+    val monos = Inductive.get_monos lthy;
+    val eqvt_thms = NominalThmDecls.get_eqvt_thms lthy;
     val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
     val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
-      (Induct.lookup_inductP ctxt (hd names)))));
-    val (raw_induct', ctxt') = ctxt
+      (Induct.lookup_inductP lthy (hd names)))));
+    val (raw_induct', ctxt') = lthy
       |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
       HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
@@ -275,10 +275,11 @@
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
       ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
-    val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
-      addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-      addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
-        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
+    fun eqvt_ss ctxt =
+      put_simpset HOL_basic_ss ctxt
+        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
+        addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
+          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
     val perm_bij = Global_Theory.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => Global_Theory.get_thm thy
@@ -299,26 +300,26 @@
             (HOLogic.exists_const T $ Abs ("x", T,
               NominalDatatype.fresh_const T (fastype_of p) $
                 Bound 0 $ p)))
-          (fn _ => EVERY
-            [resolve_tac ctxt exists_fresh' 1,
-             resolve_tac ctxt fs_atoms 1]);
+          (fn {context = goal_ctxt, ...} => EVERY
+            [resolve_tac goal_ctxt exists_fresh' 1,
+             resolve_tac goal_ctxt fs_atoms 1]);
         val (([(_, cx)], ths), ctxt') = Obtain.result
-          (fn ctxt' => EVERY
-            [eresolve_tac ctxt' [exE] 1,
-             full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
-             full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
-             REPEAT (eresolve_tac ctxt [conjE] 1)])
+          (fn goal_ctxt => EVERY
+            [eresolve_tac goal_ctxt [exE] 1,
+             full_simp_tac (put_simpset HOL_ss goal_ctxt addsimps (fresh_prod :: fresh_atm)) 1,
+             full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps [@{thm id_apply}]) 1,
+             REPEAT (eresolve_tac goal_ctxt [conjE] 1)])
           [ex] ctxt
       in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end;
 
-    fun mk_ind_proof ctxt' thss =
-      Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
-        let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
-          resolve_tac context [raw_induct] 1 THEN
+    fun mk_ind_proof ctxt thss =
+      Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} =>
+        let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} =>
+          resolve_tac goal_ctxt1 [raw_induct] 1 THEN
           EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
-            [REPEAT (resolve_tac context [allI] 1),
-             simp_tac (put_simpset eqvt_ss context) 1,
-             SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
+            [REPEAT (resolve_tac goal_ctxt1 [allI] 1),
+             simp_tac (eqvt_ss goal_ctxt1) 1,
+             SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} =>
                let
                  val (params', (pis, z)) =
                    chop (length params - length atomTs - 1) (map (Thm.term_of o #2) params) ||>
@@ -329,9 +330,9 @@
                  val pi_bvars = map (fn (t, _) =>
                    fold_rev (NominalDatatype.mk_perm []) pis t) bvars';
                  val (P, ts) = strip_comb (HOLogic.dest_Trueprop (Thm.term_of concl));
-                 val (freshs1, freshs2, ctxt'') = fold
+                 val (freshs1, freshs2, ctxt') = fold
                    (obtain_fresh_name (ts @ pi_bvars))
-                   (map snd bvars') ([], [], ctxt');
+                   (map snd bvars') ([], [], goal_ctxt2);
                  val freshs2' = NominalDatatype.mk_not_sym freshs2;
                  val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
                  fun concat_perm pi1 pi2 =
@@ -351,7 +352,7 @@
                  fun mk_pi th =
                    Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
-                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
+                     (Simplifier.simplify (eqvt_ss ctxt')
                        (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
                          (rev pis' @ pis) th));
                  val (gprems1, gprems2) = split_list
@@ -371,51 +372,54 @@
                            (fn t => fn u => fresh $ t $ u, lhs, rhs)
                        | _ $ (_ $ (_ $ lhs $ rhs)) =>
                            (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
-                     val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
+                     val th'' = Goal.prove ctxt' [] [] (HOLogic.mk_Trueprop
                          (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
                             (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
-                       (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps
-                          (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt' [th'] 1)
-                   in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end)
+                       (fn {context = goal_ctxt3, ...} =>
+                         simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps
+                          (fresh_bij @ perm_bij)) 1 THEN resolve_tac goal_ctxt3 [th'] 1)
+                   in Simplifier.simplify (eqvt_ss ctxt' addsimps fresh_atm) th'' end)
                      vc_compat_ths;
                  val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
                  (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
                  (** we have to pre-simplify the rewrite rules                   **)
-                 val swap_simps_simpset = put_simpset HOL_ss ctxt'' addsimps swap_simps @
-                    map (Simplifier.simplify (put_simpset HOL_ss ctxt'' addsimps swap_simps))
+                 val swap_simps_simpset = put_simpset HOL_ss ctxt' addsimps swap_simps @
+                    map (Simplifier.simplify (put_simpset HOL_ss ctxt' addsimps swap_simps))
                       (vc_compat_ths'' @ freshs2');
-                 val th = Goal.prove ctxt'' [] []
+                 val th = Goal.prove ctxt' [] []
                    (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
                      map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
-                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
-                     resolve_tac ctxt'' [ihyp'] 1,
+                   (fn {context = goal_ctxt4, ...} =>
+                     EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1,
+                     resolve_tac goal_ctxt4 [ihyp'] 1,
                      REPEAT_DETERM_N (Thm.nprems_of ihyp - length gprems)
                        (simp_tac swap_simps_simpset 1),
                      REPEAT_DETERM_N (length gprems)
-                       (simp_tac (put_simpset HOL_basic_ss ctxt''
+                       (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
                           addsimps [inductive_forall_def']
                           addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
-                        resolve_tac ctxt'' gprems2 1)]));
-                 val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
-                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
+                        resolve_tac goal_ctxt4 gprems2 1)]));
+                 val final = Goal.prove ctxt' [] [] (Thm.term_of concl)
+                   (fn {context = goal_ctxt5, ...} =>
+                     cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5
                      addsimps vc_compat_ths'' @ freshs2' @
                        perm_fresh_fresh @ fresh_atm) 1);
-                 val final' = Proof_Context.export ctxt'' ctxt' [final];
-               in resolve_tac ctxt' final' 1 end) context 1])
+                 val final' = Proof_Context.export ctxt' goal_ctxt2 [final];
+               in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1])
                  (prems ~~ thss ~~ ihyps ~~ prems'')))
         in
-          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt [conjE] 1) THEN
-          REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN
-            eresolve_tac ctxt [impE] 1 THEN assume_tac ctxt 1 THEN
-            REPEAT (eresolve_tac ctxt @{thms allE_Nil} 1) THEN
-            asm_full_simp_tac ctxt 1)
-        end) |> singleton (Proof_Context.export ctxt' ctxt);
+          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN
+          REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN
+            eresolve_tac goal_ctxt [impE] 1 THEN assume_tac goal_ctxt 1 THEN
+            REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN
+            asm_full_simp_tac goal_ctxt 1)
+        end) |> singleton (Proof_Context.export ctxt lthy);
 
     (** strong case analysis rule **)
 
     val cases_prems = map (fn ((name, avoids), rule) =>
       let
-        val ([rule'], ctxt') = Variable.import_terms false [Thm.prop_of rule] ctxt;
+        val ([rule'], ctxt') = Variable.import_terms false [Thm.prop_of rule] lthy;
         val prem :: prems = Logic.strip_imp_prems rule';
         val concl = Logic.strip_imp_concl rule'
       in
@@ -460,18 +464,17 @@
                    concl))
           in map mk_prem prems end) cases_prems;
 
-    val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy)
-      addsimps eqvt_thms @ swap_simps @ perm_pi_simp
-      addsimprocs [NominalPermeq.perm_simproc_app,
-        NominalPermeq.perm_simproc_fun];
+    fun cases_eqvt_simpset ctxt =
+      put_simpset HOL_ss ctxt
+        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
+        addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
 
-    val simp_fresh_atm = map
-      (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
-        addsimps fresh_atm));
+    fun simp_fresh_atm ctxt =
+      Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
 
-    fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
+    fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt))),
         prems') =
-      (name, Goal.prove ctxt' [] (prem :: prems') concl
+      (name, Goal.prove ctxt [] (prem :: prems') concl
         (fn {prems = hyp :: hyps, context = ctxt1} =>
         EVERY (resolve_tac ctxt1 [hyp RS elim] 1 ::
           map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
@@ -529,8 +532,8 @@
                        SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} =>
                          let
                            val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
-                           val case_simpset = cases_eqvt_simpset addsimps freshs2' @
-                             simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
+                           val case_simpset = cases_eqvt_simpset ctxt5 addsimps freshs2' @
+                             map (simp_fresh_atm ctxt5) (vc_compat_ths' @ fresh_hyps');
                            val fresh_fresh_simpset = case_simpset addsimps perm_fresh_fresh;
                            val hyps1' = map
                              (mk_pis #> Simplifier.simplify fresh_fresh_simpset) hyps1;
@@ -545,22 +548,22 @@
                   val final = Proof_Context.export ctxt3 ctxt2 [th]
                 in resolve_tac ctxt2 final 1 end) ctxt1 1)
                   (thss ~~ hyps ~~ prems))) |>
-                  singleton (Proof_Context.export ctxt' ctxt))
+                  singleton (Proof_Context.export ctxt lthy))
 
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
+    Proof.theorem NONE (fn thss => fn lthy1 =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = Rule_Cases.case_names induct_cases;
         val induct_cases' = Inductive.partition_rules' raw_induct
           (intrs ~~ induct_cases); 
-        val thss' = map (map (atomize_intr ctxt)) thss;
+        val thss' = map (map (atomize_intr lthy1)) thss;
         val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
         val strong_raw_induct =
-          mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
-        val strong_cases = map (mk_cases_proof ##> Inductive.rulify ctxt)
+          mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
+        val strong_cases = map (mk_cases_proof ##> Inductive.rulify lthy1)
           (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
         val strong_induct_atts =
           map (Attrib.internal o K)
@@ -568,12 +571,12 @@
         val strong_induct =
           if length names > 1 then strong_raw_induct
           else strong_raw_induct RSN (2, rev_mp);
-        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
+        val ((_, [strong_induct']), lthy2) = lthy1 |> Local_Theory.note
           ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
         val strong_inducts =
-          Project_Rule.projects ctxt (1 upto length names) strong_induct';
+          Project_Rule.projects lthy1 (1 upto length names) strong_induct';
       in
-        ctxt' |>
+        lthy2 |>
         Local_Theory.notes
           [((rec_qualified (Binding.name "strong_inducts"), []),
             strong_inducts |> map (fn th => ([th],
@@ -588,15 +591,15 @@
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;
 
-fun prove_eqvt s xatoms ctxt =  (* FIXME ctxt should be called lthy *)
+fun prove_eqvt s xatoms lthy =
   let
-    val thy = Proof_Context.theory_of ctxt;
+    val thy = Proof_Context.theory_of lthy;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
-    val raw_induct = atomize_induct ctxt raw_induct;
-    val elims = map (atomize_induct ctxt) elims;
-    val intrs = map (atomize_intr ctxt) intrs;
-    val monos = Inductive.get_monos ctxt;
+      Inductive.the_inductive_global lthy (Sign.intern_const thy s);
+    val raw_induct = atomize_induct lthy raw_induct;
+    val elims = map (atomize_induct lthy) elims;
+    val intrs = map (atomize_intr lthy) intrs;
+    val monos = Inductive.get_monos lthy;
     val intrs' = Inductive.unpartition_rules intrs
       (map (fn (((s, ths), (_, k)), th) =>
            (s, ths ~~ Inductive.infer_intro_vars thy th k ths))
@@ -617,43 +620,43 @@
          atoms)
       end;
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
-    val (([t], [pi]), ctxt') = ctxt |>
+    val (([t], [pi]), ctxt1) = lthy |>
       Variable.import_terms false [Thm.concl_of raw_induct] ||>>
       Variable.variant_fixes ["pi"];
-    val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps
-      (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs
+    fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps
+      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
       [mk_perm_bool_simproc names,
        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val ps = map (fst o HOLogic.dest_imp)
       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
-    fun eqvt_tac pi (intr, vs) st =
+    fun eqvt_tac ctxt pi (intr, vs) st =
       let
         fun eqvt_err s =
-          let val ([t], ctxt'') = Variable.import_terms true [Thm.prop_of intr] ctxt'
+          let val ([t], ctxt') = Variable.import_terms true [Thm.prop_of intr] ctxt
           in error ("Could not prove equivariance for introduction rule\n" ^
-            Syntax.string_of_term ctxt'' t ^ "\n" ^ s)
+            Syntax.string_of_term ctxt' t ^ "\n" ^ s)
           end;
-        val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
+        val res = SUBPROOF (fn {context = goal_ctxt, prems, params, ...} =>
           let
-            val prems' = map (fn th => the_default th (map_thm ctxt''
-              (split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems;
-            val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
-              (mk_perm_bool ctxt'' (Thm.cterm_of ctxt'' pi) th)) prems';
-            val intr' = infer_instantiate ctxt'' (map (#1 o dest_Var) vs ~~
-               map (Thm.cterm_of ctxt'' o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
+            val prems' = map (fn th => the_default th (map_thm goal_ctxt
+              (split_conj (K I) names) (eresolve_tac goal_ctxt [conjunct2] 1) monos NONE th)) prems;
+            val prems'' = map (fn th => Simplifier.simplify (eqvt_simpset goal_ctxt)
+              (mk_perm_bool goal_ctxt (Thm.cterm_of goal_ctxt pi) th)) prems';
+            val intr' = infer_instantiate goal_ctxt (map (#1 o dest_Var) vs ~~
+               map (Thm.cterm_of goal_ctxt o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
                intr
-          in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
-          end) ctxt' 1 st
+          in (resolve_tac goal_ctxt [intr'] THEN_ALL_NEW (TRY o resolve_tac goal_ctxt prems'')) 1
+          end) ctxt 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
           NONE => eqvt_err ("Rule does not match goal\n" ^
-            Syntax.string_of_term ctxt' (hd (Thm.prems_of st)))
+            Syntax.string_of_term ctxt (hd (Thm.prems_of st)))
         | SOME (th, _) => Seq.single th
       end;
     val thss = map (fn atom =>
       let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
       in map (fn th => zero_var_indexes (th RS mp))
-        (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
+        (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt1 [] []
           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
             let
               val (h, ts) = strip_comb p;
@@ -662,13 +665,14 @@
               HOLogic.mk_imp (p, list_comb (h, ts1 @
                 map (NominalDatatype.mk_perm [] pi') ts2))
             end) ps)))
-          (fn _ => EVERY (resolve_tac ctxt' [raw_induct] 1 :: map (fn intr_vs =>
-              full_simp_tac eqvt_simpset 1 THEN
-              eqvt_tac pi' intr_vs) intrs')) |>
-          singleton (Proof_Context.export ctxt' ctxt)))
+          (fn {context = goal_ctxt, ...} =>
+            EVERY (resolve_tac goal_ctxt [raw_induct] 1 :: map (fn intr_vs =>
+              full_simp_tac (eqvt_simpset goal_ctxt) 1 THEN
+              eqvt_tac goal_ctxt pi' intr_vs) intrs')) |>
+          singleton (Proof_Context.export ctxt1 lthy)))
       end) atoms
   in
-    ctxt |>
+    lthy |>
     Local_Theory.notes (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -26,7 +26,7 @@
     (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
+  (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt));
 
 fun fresh_postprocess ctxt =
   Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps
@@ -136,10 +136,10 @@
   let
     val prop = Thm.prop_of th;
     fun prove t =
-      Goal.prove ctxt [] [] t (fn _ =>
-        EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1,
-          REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
-          REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))])
+      Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} =>
+        EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1,
+          REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)),
+          REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))])
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
 fun abs_params params t =
@@ -153,25 +153,25 @@
     Thm.instantiate (TVars.empty, Vars.make (map (dest_Var o Envir.subst_term env) vs ~~ cts)) th
   end;
 
-fun prove_strong_ind s alt_name avoids ctxt =
+fun prove_strong_ind s alt_name avoids lthy =
   let
-    val thy = Proof_Context.theory_of ctxt;
+    val thy = Proof_Context.theory_of lthy;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global lthy (Sign.intern_const thy s);
     val ind_params = Inductive.params_of raw_induct;
-    val raw_induct = atomize_induct ctxt raw_induct;
-    val elims = map (atomize_induct ctxt) elims;
-    val monos = Inductive.get_monos ctxt;
-    val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
+    val raw_induct = atomize_induct lthy raw_induct;
+    val elims = map (atomize_induct lthy) elims;
+    val monos = Inductive.get_monos lthy;
+    val eqvt_thms = NominalThmDecls.get_eqvt_thms lthy;
     val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
     val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
-      (Induct.lookup_inductP ctxt (hd names)))));
+      (Induct.lookup_inductP lthy (hd names)))));
     val induct_cases' = if null induct_cases then replicate (length intrs) ""
       else induct_cases;
-    val (raw_induct', ctxt') = ctxt
+    val (raw_induct', ctxt') = lthy
       |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
       HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
@@ -186,7 +186,7 @@
     fun mk_avoids params name sets =
       let
         val (_, ctxt') = Proof_Context.add_fixes
-          (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
+          (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) lthy;
         fun mk s =
           let
             val t = Syntax.read_term ctxt' s;
@@ -294,10 +294,11 @@
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn a => Global_Theory.get_thm thy
       ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
-    val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
-      addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-      addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
-        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
+    fun eqvt_ss ctxt =
+      put_simpset HOL_basic_ss ctxt
+        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
+        addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
+          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
     val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
     val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
@@ -343,22 +344,23 @@
             (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
                (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
                   (pis1 @ pi :: pis2) l $ r)))
-            (fn _ => cut_facts_tac [th2] 1 THEN
-               full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |>
-          Simplifier.simplify (put_simpset eqvt_ss ctxt')
+            (fn {context = goal_ctxt, ...} =>
+              cut_facts_tac [th2] 1 THEN
+              full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps perm_set_forget) 1) |>
+          Simplifier.simplify (eqvt_ss ctxt')
       in
         (freshs @ [Thm.term_of cx],
          ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
       end;
 
-    fun mk_ind_proof ctxt' thss =
-      Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
-        let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
-          resolve_tac ctxt [raw_induct] 1 THEN
+    fun mk_ind_proof ctxt thss =
+      Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} =>
+        let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} =>
+          resolve_tac goal_ctxt1 [raw_induct] 1 THEN
           EVERY (maps (fn (((((_, sets, oprems, _),
               vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) =>
-            [REPEAT (resolve_tac ctxt [allI] 1), simp_tac (put_simpset eqvt_ss context) 1,
-             SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
+            [REPEAT (resolve_tac goal_ctxt1 [allI] 1), simp_tac (eqvt_ss goal_ctxt1) 1,
+             SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} =>
                let
                  val (cparams', (pis, z)) =
                    chop (length params - length atomTs - 1) (map #2 params) ||>
@@ -371,8 +373,8 @@
                  val gprems1 = map_filter (fn (th, t) =>
                    if null (preds_of ps t) then SOME th
                    else
-                     map_thm ctxt' (split_conj (K o I) names)
-                       (eresolve_tac ctxt' [conjunct1] 1) monos NONE th)
+                     map_thm goal_ctxt2 (split_conj (K o I) names)
+                       (eresolve_tac goal_ctxt2 [conjunct1] 1) monos NONE th)
                    (gprems ~~ oprems);
                  val vc_compat_ths' = map2 (fn th => fn p =>
                    let
@@ -380,20 +382,21 @@
                      val (h, ts) =
                        strip_comb (HOLogic.dest_Trueprop (Thm.concl_of th'))
                    in
-                     Goal.prove ctxt' [] []
+                     Goal.prove goal_ctxt2 [] []
                        (HOLogic.mk_Trueprop (list_comb (h,
                           map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
-                       (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps
-                          (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac ctxt' [th'] 1)
+                       (fn {context = goal_ctxt3, ...} =>
+                         simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps
+                          (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac goal_ctxt3 [th'] 1)
                    end) vc_compat_ths vc_compat_vs;
                  val (vc_compat_ths1, vc_compat_ths2) =
                    chop (length vc_compat_ths - length sets) vc_compat_ths';
                  val vc_compat_ths1' = map
                    (Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
-                      (Simplifier.rewrite (put_simpset eqvt_ss ctxt'))))) vc_compat_ths1;
+                      (Simplifier.rewrite (eqvt_ss goal_ctxt2))))) vc_compat_ths1;
                  val (pis', fresh_ths1, fresh_ths2, fresh_ths3, ctxt'') = fold
                    (obtain_fresh_name ts sets)
-                   (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], ctxt');
+                   (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], goal_ctxt2);
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1
                    in if T = fastype_of pi2 then
@@ -405,16 +408,17 @@
                    (map (fold_rev (NominalDatatype.mk_perm [])
                       (pis' @ pis) #> Thm.global_cterm_of thy) params' @ [Thm.global_cterm_of thy z]);
                  fun mk_pi th =
-                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
+                   Simplifier.simplify
+                     (put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
-                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
-                       (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
+                     (Simplifier.simplify (eqvt_ss ctxt'')
+                       (fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'')
                          (pis' @ pis) th));
                  val gprems2 = map (fn (th, t) =>
                    if null (preds_of ps t) then mk_pi th
                    else
-                     mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
-                       (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))
+                     mk_pi (the (map_thm ctxt'' (inst_conj_all names ps (rev pis''))
+                       (inst_conj_all_tac ctxt'' (length pis'')) monos (SOME t) th)))
                    (gprems ~~ oprems);
                  val perm_freshs_freshs' = map (fn (th, (_, T)) =>
                    th RS the (AList.lookup op = perm_freshs_freshs T))
@@ -422,44 +426,45 @@
                  val th = Goal.prove ctxt'' [] []
                    (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
                      map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
-                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1,
-                     resolve_tac ctxt'' [ihyp'] 1] @
-                     map (fn th => resolve_tac ctxt'' [th] 1) fresh_ths3 @
+                   (fn {context = goal_ctxt4, ...} =>
+                     EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1,
+                     resolve_tac goal_ctxt4 [ihyp'] 1] @
+                     map (fn th => resolve_tac goal_ctxt4 [th] 1) fresh_ths3 @
                      [REPEAT_DETERM_N (length gprems)
-                       (simp_tac (put_simpset HOL_basic_ss ctxt''
+                       (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
                           addsimps [inductive_forall_def']
                           addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
-                        resolve_tac ctxt'' gprems2 1)]));
+                        resolve_tac goal_ctxt4 gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
-                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
+                   (fn {context = goal_ctxt5, ...} =>
+                     cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5
                      addsimps vc_compat_ths1' @ fresh_ths1 @
                        perm_freshs_freshs') 1);
-                 val final' = Proof_Context.export ctxt'' ctxt' [final];
-               in resolve_tac ctxt' final' 1 end) context 1])
+                 val final' = Proof_Context.export ctxt'' goal_ctxt2 [final];
+               in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1])
                  (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems'')))
         in
-          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt' [conjE] 1) THEN
-          REPEAT (REPEAT (resolve_tac ctxt' [conjI, impI] 1) THEN
-            eresolve_tac ctxt' [impE] 1 THEN
-            assume_tac ctxt' 1 THEN REPEAT (eresolve_tac ctxt' @{thms allE_Nil} 1) THEN
-            asm_full_simp_tac ctxt 1)
+          cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN
+          REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN
+            eresolve_tac goal_ctxt [impE] 1 THEN
+            assume_tac goal_ctxt 1 THEN REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN
+            asm_full_simp_tac goal_ctxt 1)
         end) |>
-        fresh_postprocess ctxt' |>
-        singleton (Proof_Context.export ctxt' ctxt);
-
+        fresh_postprocess ctxt |>
+        singleton (Proof_Context.export ctxt lthy);
   in
     ctxt'' |>
-    Proof.theorem NONE (fn thss => fn ctxt =>  (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
+    Proof.theorem NONE (fn thss => fn lthy1 =>
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = Rule_Cases.case_names induct_cases;
         val induct_cases' = Inductive.partition_rules' raw_induct
           (intrs ~~ induct_cases); 
-        val thss' = map (map (atomize_intr ctxt)) thss;
+        val thss' = map (map (atomize_intr lthy1)) thss;
         val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
         val strong_raw_induct =
-          mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
+          mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
         val strong_induct_atts =
           map (Attrib.internal o K)
             [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
@@ -471,12 +476,12 @@
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
-        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
+        val ((_, [strong_induct']), lthy2) = lthy1 |> Local_Theory.note
           ((induct_name, strong_induct_atts), [strong_induct]);
         val strong_inducts =
-          Project_Rule.projects ctxt' (1 upto length names) strong_induct'
+          Project_Rule.projects lthy2 (1 upto length names) strong_induct'
       in
-        ctxt' |>
+        lthy2 |>
         Local_Theory.notes [((inducts_name, []),
           strong_inducts |> map (fn th => ([th],
             [Attrib.internal (K ind_case_names),
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Mon Oct 18 18:33:46 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 (SOME 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
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Mon Oct 18 18:33:46 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'
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Oct 18 18:33:46 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));
 
 
--- a/src/HOL/Tools/Function/function_core.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -622,8 +622,8 @@
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (Conv.binder_conv
-              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
+            fconv_rule
+              (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
--- a/src/HOL/Tools/Function/function_lib.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Mon Oct 18 18:33:46 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')
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 18 18:33:46 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 NONE 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
@@ -135,14 +135,14 @@
         | _ => raise Fail "abstract: Bad term"
   end;
 
-(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
+(* Traverse a theorem, replacing lambda-abstractions with combinators. *)
 fun introduce_combinators_in_cterm ctxt ct =
   if is_quasi_lambda_free (Thm.term_of ct) then
     Thm.reflexive ct
   else case Thm.term_of ct of
     Abs _ =>
     let
-      val (cv, cta) = Thm.dest_abs NONE 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 NONE 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 (SOME s') #> snd #> zap pos
+          Thm.dest_comb #> snd #> Thm.dest_abs_global #> snd #> zap pos
         else
           Conv.all_conv
       | Const (s, _) $ _ $ _ =>
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -145,7 +145,7 @@
 
 fun get_pmi_term t =
   let val (x,eq) =
-     (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE 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 NONE
+  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 NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
-    |> Thm.dest_abs NONE |> 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 NONE (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
@@ -640,7 +640,7 @@
   | fm_of_term ps vs (\<^term>\<open>(=) :: bool => _ \<close> $ t1 $ t2) =
       Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (Const (\<^const_name>\<open>Not\<close>, _) $ t') =
-      Proc.NOT (fm_of_term ps vs t')
+      Proc.Not (fm_of_term ps vs t')
   | fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs abs) =
       Proc.E (uncurry (fm_of_term ps) (descend vs abs))
   | fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs abs) =
@@ -677,18 +677,18 @@
   | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   | term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\<open>(=) :: bool => _\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
-  | term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t'
+  | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
   | term_of_fm ps vs (Proc.Eq t') = \<^term>\<open>(=) :: int => _ \<close> $ term_of_num vs t'$ \<^term>\<open>0::int\<close>
-  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t'))
+  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
   | term_of_fm ps vs (Proc.Lt t') = \<^term>\<open>(<) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
   | term_of_fm ps vs (Proc.Le t') = \<^term>\<open>(<=) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close>
   | term_of_fm ps vs (Proc.Gt t') = \<^term>\<open>(<) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
   | term_of_fm ps vs (Proc.Ge t') = \<^term>\<open>(<=) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t'
   | term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\<open>(dvd) :: int => _ \<close> $
       HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t'
-  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t')))
+  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
   | term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n)
-  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n));
+  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
 
 fun procedure t =
   let
@@ -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 (SOME 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 NONE 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;
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -7,7 +7,7 @@
     Neg of numa | Add of numa * numa | Sub of numa * numa | Mul of inta * numa
   datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
     Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
-    NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
+    Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm
     | E of fm | A of fm | Closed of nat | NClosed of nat
   val pa : fm -> fm
   val nat_of_integer : int -> nat
@@ -619,7 +619,7 @@
 
 datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa |
   Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa |
-  NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
+  Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm |
   E of fm | A of fm | Closed of nat | NClosed of nat;
 
 fun id x = (fn xa => xa) x;
@@ -643,7 +643,7 @@
   | disjuncts (NEq v) = [NEq v]
   | disjuncts (Dvd (v, va)) = [Dvd (v, va)]
   | disjuncts (NDvd (v, va)) = [NDvd (v, va)]
-  | disjuncts (NOT v) = [NOT v]
+  | disjuncts (Not v) = [Not v]
   | disjuncts (And (v, va)) = [And (v, va)]
   | disjuncts (Imp (v, va)) = [Imp (v, va)]
   | disjuncts (Iff (v, va)) = [Iff (v, va)]
@@ -711,22 +711,22 @@
   | equal_fm (Imp (x141, x142)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Or (x131, x132)) = false
   | equal_fm (Or (x131, x132)) (And (x121, x122)) = false
-  | equal_fm (NOT x11) (NClosed x19) = false
-  | equal_fm (NClosed x19) (NOT x11) = false
-  | equal_fm (NOT x11) (Closed x18) = false
-  | equal_fm (Closed x18) (NOT x11) = false
-  | equal_fm (NOT x11) (A x17) = false
-  | equal_fm (A x17) (NOT x11) = false
-  | equal_fm (NOT x11) (E x16) = false
-  | equal_fm (E x16) (NOT x11) = false
-  | equal_fm (NOT x11) (Iff (x151, x152)) = false
-  | equal_fm (Iff (x151, x152)) (NOT x11) = false
-  | equal_fm (NOT x11) (Imp (x141, x142)) = false
-  | equal_fm (Imp (x141, x142)) (NOT x11) = false
-  | equal_fm (NOT x11) (Or (x131, x132)) = false
-  | equal_fm (Or (x131, x132)) (NOT x11) = false
-  | equal_fm (NOT x11) (And (x121, x122)) = false
-  | equal_fm (And (x121, x122)) (NOT x11) = false
+  | equal_fm (Not x11) (NClosed x19) = false
+  | equal_fm (NClosed x19) (Not x11) = false
+  | equal_fm (Not x11) (Closed x18) = false
+  | equal_fm (Closed x18) (Not x11) = false
+  | equal_fm (Not x11) (A x17) = false
+  | equal_fm (A x17) (Not x11) = false
+  | equal_fm (Not x11) (E x16) = false
+  | equal_fm (E x16) (Not x11) = false
+  | equal_fm (Not x11) (Iff (x151, x152)) = false
+  | equal_fm (Iff (x151, x152)) (Not x11) = false
+  | equal_fm (Not x11) (Imp (x141, x142)) = false
+  | equal_fm (Imp (x141, x142)) (Not x11) = false
+  | equal_fm (Not x11) (Or (x131, x132)) = false
+  | equal_fm (Or (x131, x132)) (Not x11) = false
+  | equal_fm (Not x11) (And (x121, x122)) = false
+  | equal_fm (And (x121, x122)) (Not x11) = false
   | equal_fm (NDvd (x101, x102)) (NClosed x19) = false
   | equal_fm (NClosed x19) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Closed x18) = false
@@ -743,8 +743,8 @@
   | equal_fm (Or (x131, x132)) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (NDvd (x101, x102)) = false
-  | equal_fm (NDvd (x101, x102)) (NOT x11) = false
-  | equal_fm (NOT x11) (NDvd (x101, x102)) = false
+  | equal_fm (NDvd (x101, x102)) (Not x11) = false
+  | equal_fm (Not x11) (NDvd (x101, x102)) = false
   | equal_fm (Dvd (x91, x92)) (NClosed x19) = false
   | equal_fm (NClosed x19) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (Closed x18) = false
@@ -761,8 +761,8 @@
   | equal_fm (Or (x131, x132)) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Dvd (x91, x92)) = false
-  | equal_fm (Dvd (x91, x92)) (NOT x11) = false
-  | equal_fm (NOT x11) (Dvd (x91, x92)) = false
+  | equal_fm (Dvd (x91, x92)) (Not x11) = false
+  | equal_fm (Not x11) (Dvd (x91, x92)) = false
   | equal_fm (Dvd (x91, x92)) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Dvd (x91, x92)) = false
   | equal_fm (NEq x8) (NClosed x19) = false
@@ -781,8 +781,8 @@
   | equal_fm (Or (x131, x132)) (NEq x8) = false
   | equal_fm (NEq x8) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (NEq x8) = false
-  | equal_fm (NEq x8) (NOT x11) = false
-  | equal_fm (NOT x11) (NEq x8) = false
+  | equal_fm (NEq x8) (Not x11) = false
+  | equal_fm (Not x11) (NEq x8) = false
   | equal_fm (NEq x8) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (NEq x8) = false
   | equal_fm (NEq x8) (Dvd (x91, x92)) = false
@@ -803,8 +803,8 @@
   | equal_fm (Or (x131, x132)) (Eq x7) = false
   | equal_fm (Eq x7) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Eq x7) = false
-  | equal_fm (Eq x7) (NOT x11) = false
-  | equal_fm (NOT x11) (Eq x7) = false
+  | equal_fm (Eq x7) (Not x11) = false
+  | equal_fm (Not x11) (Eq x7) = false
   | equal_fm (Eq x7) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Eq x7) = false
   | equal_fm (Eq x7) (Dvd (x91, x92)) = false
@@ -827,8 +827,8 @@
   | equal_fm (Or (x131, x132)) (Ge x6) = false
   | equal_fm (Ge x6) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Ge x6) = false
-  | equal_fm (Ge x6) (NOT x11) = false
-  | equal_fm (NOT x11) (Ge x6) = false
+  | equal_fm (Ge x6) (Not x11) = false
+  | equal_fm (Not x11) (Ge x6) = false
   | equal_fm (Ge x6) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Ge x6) = false
   | equal_fm (Ge x6) (Dvd (x91, x92)) = false
@@ -853,8 +853,8 @@
   | equal_fm (Or (x131, x132)) (Gt x5) = false
   | equal_fm (Gt x5) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Gt x5) = false
-  | equal_fm (Gt x5) (NOT x11) = false
-  | equal_fm (NOT x11) (Gt x5) = false
+  | equal_fm (Gt x5) (Not x11) = false
+  | equal_fm (Not x11) (Gt x5) = false
   | equal_fm (Gt x5) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Gt x5) = false
   | equal_fm (Gt x5) (Dvd (x91, x92)) = false
@@ -881,8 +881,8 @@
   | equal_fm (Or (x131, x132)) (Le x4) = false
   | equal_fm (Le x4) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Le x4) = false
-  | equal_fm (Le x4) (NOT x11) = false
-  | equal_fm (NOT x11) (Le x4) = false
+  | equal_fm (Le x4) (Not x11) = false
+  | equal_fm (Not x11) (Le x4) = false
   | equal_fm (Le x4) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Le x4) = false
   | equal_fm (Le x4) (Dvd (x91, x92)) = false
@@ -911,8 +911,8 @@
   | equal_fm (Or (x131, x132)) (Lt x3) = false
   | equal_fm (Lt x3) (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) (Lt x3) = false
-  | equal_fm (Lt x3) (NOT x11) = false
-  | equal_fm (NOT x11) (Lt x3) = false
+  | equal_fm (Lt x3) (Not x11) = false
+  | equal_fm (Not x11) (Lt x3) = false
   | equal_fm (Lt x3) (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) (Lt x3) = false
   | equal_fm (Lt x3) (Dvd (x91, x92)) = false
@@ -943,8 +943,8 @@
   | equal_fm (Or (x131, x132)) F = false
   | equal_fm F (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) F = false
-  | equal_fm F (NOT x11) = false
-  | equal_fm (NOT x11) F = false
+  | equal_fm F (Not x11) = false
+  | equal_fm (Not x11) F = false
   | equal_fm F (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) F = false
   | equal_fm F (Dvd (x91, x92)) = false
@@ -977,8 +977,8 @@
   | equal_fm (Or (x131, x132)) T = false
   | equal_fm T (And (x121, x122)) = false
   | equal_fm (And (x121, x122)) T = false
-  | equal_fm T (NOT x11) = false
-  | equal_fm (NOT x11) T = false
+  | equal_fm T (Not x11) = false
+  | equal_fm (Not x11) T = false
   | equal_fm T (NDvd (x101, x102)) = false
   | equal_fm (NDvd (x101, x102)) T = false
   | equal_fm T (Dvd (x91, x92)) = false
@@ -1009,7 +1009,7 @@
     equal_fm x131 y131 andalso equal_fm x132 y132
   | equal_fm (And (x121, x122)) (And (y121, y122)) =
     equal_fm x121 y121 andalso equal_fm x122 y122
-  | equal_fm (NOT x11) (NOT y11) = equal_fm x11 y11
+  | equal_fm (Not x11) (Not y11) = equal_fm x11 y11
   | equal_fm (NDvd (x101, x102)) (NDvd (y101, y102)) =
     equal_inta x101 y101 andalso equal_numa x102 y102
   | equal_fm (Dvd (x91, x92)) (Dvd (y91, y92)) =
@@ -1030,7 +1030,7 @@
                   | Le _ => Or (f p, q) | Gt _ => Or (f p, q)
                   | Ge _ => Or (f p, q) | Eq _ => Or (f p, q)
                   | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q)
-                  | NDvd (_, _) => Or (f p, q) | NOT _ => Or (f p, q)
+                  | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q)
                   | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q)
                   | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q)
                   | E _ => Or (f p, q) | A _ => Or (f p, q)
@@ -1089,7 +1089,7 @@
   | minusinf (NEq (Mul (va, vb))) = NEq (Mul (va, vb))
   | minusinf (Dvd (v, va)) = Dvd (v, va)
   | minusinf (NDvd (v, va)) = NDvd (v, va)
-  | minusinf (NOT v) = NOT v
+  | minusinf (Not v) = Not v
   | minusinf (Imp (v, va)) = Imp (v, va)
   | minusinf (Iff (v, va)) = Iff (v, va)
   | minusinf (E v) = E v
@@ -1138,7 +1138,7 @@
   | subst0 t (NEq a) = NEq (numsubst0 t a)
   | subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a)
   | subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a)
-  | subst0 t (NOT p) = NOT (subst0 t p)
+  | subst0 t (Not p) = Not (subst0 t p)
   | subst0 t (And (p, q)) = And (subst0 t p, subst0 t q)
   | subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q)
   | subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q)
@@ -1263,25 +1263,25 @@
     else (if equal_fm p T then q
            else (if equal_fm q T then p else And (p, q))));
 
-fun nota (NOT p) = p
+fun nota (Not p) = p
   | nota T = F
   | nota F = T
-  | nota (Lt v) = NOT (Lt v)
-  | nota (Le v) = NOT (Le v)
-  | nota (Gt v) = NOT (Gt v)
-  | nota (Ge v) = NOT (Ge v)
-  | nota (Eq v) = NOT (Eq v)
-  | nota (NEq v) = NOT (NEq v)
-  | nota (Dvd (v, va)) = NOT (Dvd (v, va))
-  | nota (NDvd (v, va)) = NOT (NDvd (v, va))
-  | nota (And (v, va)) = NOT (And (v, va))
-  | nota (Or (v, va)) = NOT (Or (v, va))
-  | nota (Imp (v, va)) = NOT (Imp (v, va))
-  | nota (Iff (v, va)) = NOT (Iff (v, va))
-  | nota (E v) = NOT (E v)
-  | nota (A v) = NOT (A v)
-  | nota (Closed v) = NOT (Closed v)
-  | nota (NClosed v) = NOT (NClosed v);
+  | nota (Lt v) = Not (Lt v)
+  | nota (Le v) = Not (Le v)
+  | nota (Gt v) = Not (Gt v)
+  | nota (Ge v) = Not (Ge v)
+  | nota (Eq v) = Not (Eq v)
+  | nota (NEq v) = Not (NEq v)
+  | nota (Dvd (v, va)) = Not (Dvd (v, va))
+  | nota (NDvd (v, va)) = Not (NDvd (v, va))
+  | nota (And (v, va)) = Not (And (v, va))
+  | nota (Or (v, va)) = Not (Or (v, va))
+  | nota (Imp (v, va)) = Not (Imp (v, va))
+  | nota (Iff (v, va)) = Not (Iff (v, va))
+  | nota (E v) = Not (E v)
+  | nota (A v) = Not (A v)
+  | nota (Closed v) = Not (Closed v)
+  | nota (NClosed v) = Not (NClosed v);
 
 fun imp p q =
   (if equal_fm p F orelse equal_fm q T then T
@@ -1301,7 +1301,7 @@
   | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q)
   | simpfm (Imp (p, q)) = imp (simpfm p) (simpfm q)
   | simpfm (Iff (p, q)) = iff (simpfm p) (simpfm q)
-  | simpfm (NOT p) = nota (simpfm p)
+  | simpfm (Not p) = nota (simpfm p)
   | simpfm (Lt a) =
     let
       val aa = simpnum a;
@@ -1442,7 +1442,7 @@
   | a_beta (NDvd (v, Add (vb, vc))) k = NDvd (v, Add (vb, vc))
   | a_beta (NDvd (v, Sub (vb, vc))) k = NDvd (v, Sub (vb, vc))
   | a_beta (NDvd (v, Mul (vb, vc))) k = NDvd (v, Mul (vb, vc))
-  | a_beta (NOT v) k = NOT v
+  | a_beta (Not v) k = Not v
   | a_beta (Imp (v, va)) k = Imp (v, va)
   | a_beta (Iff (v, va)) k = Iff (v, va)
   | a_beta (E v) k = E v
@@ -1515,7 +1515,7 @@
   | delta (NDvd (v, Add (vb, vc))) = one_inta
   | delta (NDvd (v, Sub (vb, vc))) = one_inta
   | delta (NDvd (v, Mul (vb, vc))) = one_inta
-  | delta (NOT v) = one_inta
+  | delta (Not v) = one_inta
   | delta (Imp (v, va)) = one_inta
   | delta (Iff (v, va)) = one_inta
   | delta (E v) = one_inta
@@ -1569,7 +1569,7 @@
   | alpha (NEq (Mul (va, vb))) = []
   | alpha (Dvd (v, va)) = []
   | alpha (NDvd (v, va)) = []
-  | alpha (NOT v) = []
+  | alpha (Not v) = []
   | alpha (Imp (v, va)) = []
   | alpha (Iff (v, va)) = []
   | alpha (E v) = []
@@ -1637,7 +1637,7 @@
   | zeta (NDvd (v, Add (vb, vc))) = one_inta
   | zeta (NDvd (v, Sub (vb, vc))) = one_inta
   | zeta (NDvd (v, Mul (vb, vc))) = one_inta
-  | zeta (NOT v) = one_inta
+  | zeta (Not v) = one_inta
   | zeta (Imp (v, va)) = one_inta
   | zeta (Iff (v, va)) = one_inta
   | zeta (E v) = one_inta
@@ -1697,7 +1697,7 @@
   | beta (NEq (Mul (va, vb))) = []
   | beta (Dvd (v, va)) = []
   | beta (NDvd (v, va)) = []
-  | beta (NOT v) = []
+  | beta (Not v) = []
   | beta (Imp (v, va)) = []
   | beta (Iff (v, va)) = []
   | beta (E v) = []
@@ -1766,7 +1766,7 @@
   | mirror (NDvd (v, Add (vb, vc))) = NDvd (v, Add (vb, vc))
   | mirror (NDvd (v, Sub (vb, vc))) = NDvd (v, Sub (vb, vc))
   | mirror (NDvd (v, Mul (vb, vc))) = NDvd (v, Mul (vb, vc))
-  | mirror (NOT v) = NOT v
+  | mirror (Not v) = Not v
   | mirror (Imp (v, va)) = Imp (v, va)
   | mirror (Iff (v, va)) = Iff (v, va)
   | mirror (E v) = E v
@@ -1848,9 +1848,9 @@
 
 fun zlfm (And (p, q)) = And (zlfm p, zlfm q)
   | zlfm (Or (p, q)) = Or (zlfm p, zlfm q)
-  | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q)
+  | zlfm (Imp (p, q)) = Or (zlfm (Not p), zlfm q)
   | zlfm (Iff (p, q)) =
-    Or (And (zlfm p, zlfm q), And (zlfm (NOT p), zlfm (NOT q)))
+    Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q)))
   | zlfm (Lt a) =
     let
       val (c, r) = zsplit0 a;
@@ -1920,28 +1920,28 @@
                       else NDvd (abs_int i,
                                   CN (zero_nat, uminus_int c, Neg r))))
            end)
-  | zlfm (NOT (And (p, q))) = Or (zlfm (NOT p), zlfm (NOT q))
-  | zlfm (NOT (Or (p, q))) = And (zlfm (NOT p), zlfm (NOT q))
-  | zlfm (NOT (Imp (p, q))) = And (zlfm p, zlfm (NOT q))
-  | zlfm (NOT (Iff (p, q))) =
-    Or (And (zlfm p, zlfm (NOT q)), And (zlfm (NOT p), zlfm q))
-  | zlfm (NOT (NOT p)) = zlfm p
-  | zlfm (NOT T) = F
-  | zlfm (NOT F) = T
-  | zlfm (NOT (Lt a)) = zlfm (Ge a)
-  | zlfm (NOT (Le a)) = zlfm (Gt a)
-  | zlfm (NOT (Gt a)) = zlfm (Le a)
-  | zlfm (NOT (Ge a)) = zlfm (Lt a)
-  | zlfm (NOT (Eq a)) = zlfm (NEq a)
-  | zlfm (NOT (NEq a)) = zlfm (Eq a)
-  | zlfm (NOT (Dvd (i, a))) = zlfm (NDvd (i, a))
-  | zlfm (NOT (NDvd (i, a))) = zlfm (Dvd (i, a))
-  | zlfm (NOT (Closed p)) = NClosed p
-  | zlfm (NOT (NClosed p)) = Closed p
+  | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q))
+  | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q))
+  | zlfm (Not (Imp (p, q))) = And (zlfm p, zlfm (Not q))
+  | zlfm (Not (Iff (p, q))) =
+    Or (And (zlfm p, zlfm (Not q)), And (zlfm (Not p), zlfm q))
+  | zlfm (Not (Not p)) = zlfm p
+  | zlfm (Not T) = F
+  | zlfm (Not F) = T
+  | zlfm (Not (Lt a)) = zlfm (Ge a)
+  | zlfm (Not (Le a)) = zlfm (Gt a)
+  | zlfm (Not (Gt a)) = zlfm (Le a)
+  | zlfm (Not (Ge a)) = zlfm (Lt a)
+  | zlfm (Not (Eq a)) = zlfm (NEq a)
+  | zlfm (Not (NEq a)) = zlfm (Eq a)
+  | zlfm (Not (Dvd (i, a))) = zlfm (NDvd (i, a))
+  | zlfm (Not (NDvd (i, a))) = zlfm (Dvd (i, a))
+  | zlfm (Not (Closed p)) = NClosed p
+  | zlfm (Not (NClosed p)) = Closed p
   | zlfm T = T
   | zlfm F = F
-  | zlfm (NOT (E va)) = NOT (E va)
-  | zlfm (NOT (A va)) = NOT (A va)
+  | zlfm (Not (E va)) = Not (E va)
+  | zlfm (Not (A va)) = Not (A va)
   | zlfm (E v) = E v
   | zlfm (A v) = A v
   | zlfm (Closed v) = Closed v
@@ -1976,7 +1976,7 @@
   | decr (NEq a) = NEq (decrnum a)
   | decr (Dvd (i, a)) = Dvd (i, decrnum a)
   | decr (NDvd (i, a)) = NDvd (i, decrnum a)
-  | decr (NOT p) = NOT (decr p)
+  | decr (Not p) = Not (decr p)
   | decr (And (p, q)) = And (decr p, decr q)
   | decr (Or (p, q)) = Or (decr p, decr q)
   | decr (Imp (p, q)) = Imp (decr p, decr q)
@@ -2014,8 +2014,8 @@
   end;
 
 fun qelim (E p) = (fn qe => dj qe (qelim p qe))
-  | qelim (A p) = (fn qe => nota (qe (qelim (NOT p) qe)))
-  | qelim (NOT p) = (fn qe => nota (qelim p qe))
+  | qelim (A p) = (fn qe => nota (qe (qelim (Not p) qe)))
+  | qelim (Not p) = (fn qe => nota (qelim p qe))
   | qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe))
   | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe))
   | qelim (Imp (p, q)) = (fn qe => imp (qelim p qe) (qelim q qe))
@@ -2036,13 +2036,13 @@
 fun prep (E T) = T
   | prep (E F) = F
   | prep (E (Or (p, q))) = Or (prep (E p), prep (E q))
-  | prep (E (Imp (p, q))) = Or (prep (E (NOT p)), prep (E q))
+  | prep (E (Imp (p, q))) = Or (prep (E (Not p)), prep (E q))
   | prep (E (Iff (p, q))) =
-    Or (prep (E (And (p, q))), prep (E (And (NOT p, NOT q))))
-  | prep (E (NOT (And (p, q)))) = Or (prep (E (NOT p)), prep (E (NOT q)))
-  | prep (E (NOT (Imp (p, q)))) = prep (E (And (p, NOT q)))
-  | prep (E (NOT (Iff (p, q)))) =
-    Or (prep (E (And (p, NOT q))), prep (E (And (NOT p, q))))
+    Or (prep (E (And (p, q))), prep (E (And (Not p, Not q))))
+  | prep (E (Not (And (p, q)))) = Or (prep (E (Not p)), prep (E (Not q)))
+  | prep (E (Not (Imp (p, q)))) = prep (E (And (p, Not q)))
+  | prep (E (Not (Iff (p, q)))) =
+    Or (prep (E (And (p, Not q))), prep (E (And (Not p, q))))
   | prep (E (Lt v)) = E (prep (Lt v))
   | prep (E (Le v)) = E (prep (Le v))
   | prep (E (Gt v)) = E (prep (Gt v))
@@ -2051,69 +2051,69 @@
   | prep (E (NEq v)) = E (prep (NEq v))
   | prep (E (Dvd (v, va))) = E (prep (Dvd (v, va)))
   | prep (E (NDvd (v, va))) = E (prep (NDvd (v, va)))
-  | prep (E (NOT T)) = E (prep (NOT T))
-  | prep (E (NOT F)) = E (prep (NOT F))
-  | prep (E (NOT (Lt va))) = E (prep (NOT (Lt va)))
-  | prep (E (NOT (Le va))) = E (prep (NOT (Le va)))
-  | prep (E (NOT (Gt va))) = E (prep (NOT (Gt va)))
-  | prep (E (NOT (Ge va))) = E (prep (NOT (Ge va)))
-  | prep (E (NOT (Eq va))) = E (prep (NOT (Eq va)))
-  | prep (E (NOT (NEq va))) = E (prep (NOT (NEq va)))
-  | prep (E (NOT (Dvd (va, vb)))) = E (prep (NOT (Dvd (va, vb))))
-  | prep (E (NOT (NDvd (va, vb)))) = E (prep (NOT (NDvd (va, vb))))
-  | prep (E (NOT (NOT va))) = E (prep (NOT (NOT va)))
-  | prep (E (NOT (Or (va, vb)))) = E (prep (NOT (Or (va, vb))))
-  | prep (E (NOT (E va))) = E (prep (NOT (E va)))
-  | prep (E (NOT (A va))) = E (prep (NOT (A va)))
-  | prep (E (NOT (Closed va))) = E (prep (NOT (Closed va)))
-  | prep (E (NOT (NClosed va))) = E (prep (NOT (NClosed va)))
+  | prep (E (Not T)) = E (prep (Not T))
+  | prep (E (Not F)) = E (prep (Not F))
+  | prep (E (Not (Lt va))) = E (prep (Not (Lt va)))
+  | prep (E (Not (Le va))) = E (prep (Not (Le va)))
+  | prep (E (Not (Gt va))) = E (prep (Not (Gt va)))
+  | prep (E (Not (Ge va))) = E (prep (Not (Ge va)))
+  | prep (E (Not (Eq va))) = E (prep (Not (Eq va)))
+  | prep (E (Not (NEq va))) = E (prep (Not (NEq va)))
+  | prep (E (Not (Dvd (va, vb)))) = E (prep (Not (Dvd (va, vb))))
+  | prep (E (Not (NDvd (va, vb)))) = E (prep (Not (NDvd (va, vb))))
+  | prep (E (Not (Not va))) = E (prep (Not (Not va)))
+  | prep (E (Not (Or (va, vb)))) = E (prep (Not (Or (va, vb))))
+  | prep (E (Not (E va))) = E (prep (Not (E va)))
+  | prep (E (Not (A va))) = E (prep (Not (A va)))
+  | prep (E (Not (Closed va))) = E (prep (Not (Closed va)))
+  | prep (E (Not (NClosed va))) = E (prep (Not (NClosed va)))
   | prep (E (And (v, va))) = E (prep (And (v, va)))
   | prep (E (E v)) = E (prep (E v))
   | prep (E (A v)) = E (prep (A v))
   | prep (E (Closed v)) = E (prep (Closed v))
   | prep (E (NClosed v)) = E (prep (NClosed v))
   | prep (A (And (p, q))) = And (prep (A p), prep (A q))
-  | prep (A T) = prep (NOT (E (NOT T)))
-  | prep (A F) = prep (NOT (E (NOT F)))
-  | prep (A (Lt v)) = prep (NOT (E (NOT (Lt v))))
-  | prep (A (Le v)) = prep (NOT (E (NOT (Le v))))
-  | prep (A (Gt v)) = prep (NOT (E (NOT (Gt v))))
-  | prep (A (Ge v)) = prep (NOT (E (NOT (Ge v))))
-  | prep (A (Eq v)) = prep (NOT (E (NOT (Eq v))))
-  | prep (A (NEq v)) = prep (NOT (E (NOT (NEq v))))
-  | prep (A (Dvd (v, va))) = prep (NOT (E (NOT (Dvd (v, va)))))
-  | prep (A (NDvd (v, va))) = prep (NOT (E (NOT (NDvd (v, va)))))
-  | prep (A (NOT v)) = prep (NOT (E (NOT (NOT v))))
-  | prep (A (Or (v, va))) = prep (NOT (E (NOT (Or (v, va)))))
-  | prep (A (Imp (v, va))) = prep (NOT (E (NOT (Imp (v, va)))))
-  | prep (A (Iff (v, va))) = prep (NOT (E (NOT (Iff (v, va)))))
-  | prep (A (E v)) = prep (NOT (E (NOT (E v))))
-  | prep (A (A v)) = prep (NOT (E (NOT (A v))))
-  | prep (A (Closed v)) = prep (NOT (E (NOT (Closed v))))
-  | prep (A (NClosed v)) = prep (NOT (E (NOT (NClosed v))))
-  | prep (NOT (NOT p)) = prep p
-  | prep (NOT (And (p, q))) = Or (prep (NOT p), prep (NOT q))
-  | prep (NOT (A p)) = prep (E (NOT p))
-  | prep (NOT (Or (p, q))) = And (prep (NOT p), prep (NOT q))
-  | prep (NOT (Imp (p, q))) = And (prep p, prep (NOT q))
-  | prep (NOT (Iff (p, q))) = Or (prep (And (p, NOT q)), prep (And (NOT p, q)))
-  | prep (NOT T) = NOT (prep T)
-  | prep (NOT F) = NOT (prep F)
-  | prep (NOT (Lt v)) = NOT (prep (Lt v))
-  | prep (NOT (Le v)) = NOT (prep (Le v))
-  | prep (NOT (Gt v)) = NOT (prep (Gt v))
-  | prep (NOT (Ge v)) = NOT (prep (Ge v))
-  | prep (NOT (Eq v)) = NOT (prep (Eq v))
-  | prep (NOT (NEq v)) = NOT (prep (NEq v))
-  | prep (NOT (Dvd (v, va))) = NOT (prep (Dvd (v, va)))
-  | prep (NOT (NDvd (v, va))) = NOT (prep (NDvd (v, va)))
-  | prep (NOT (E v)) = NOT (prep (E v))
-  | prep (NOT (Closed v)) = NOT (prep (Closed v))
-  | prep (NOT (NClosed v)) = NOT (prep (NClosed v))
+  | prep (A T) = prep (Not (E (Not T)))
+  | prep (A F) = prep (Not (E (Not F)))
+  | prep (A (Lt v)) = prep (Not (E (Not (Lt v))))
+  | prep (A (Le v)) = prep (Not (E (Not (Le v))))
+  | prep (A (Gt v)) = prep (Not (E (Not (Gt v))))
+  | prep (A (Ge v)) = prep (Not (E (Not (Ge v))))
+  | prep (A (Eq v)) = prep (Not (E (Not (Eq v))))
+  | prep (A (NEq v)) = prep (Not (E (Not (NEq v))))
+  | prep (A (Dvd (v, va))) = prep (Not (E (Not (Dvd (v, va)))))
+  | prep (A (NDvd (v, va))) = prep (Not (E (Not (NDvd (v, va)))))
+  | prep (A (Not v)) = prep (Not (E (Not (Not v))))
+  | prep (A (Or (v, va))) = prep (Not (E (Not (Or (v, va)))))
+  | prep (A (Imp (v, va))) = prep (Not (E (Not (Imp (v, va)))))
+  | prep (A (Iff (v, va))) = prep (Not (E (Not (Iff (v, va)))))
+  | prep (A (E v)) = prep (Not (E (Not (E v))))
+  | prep (A (A v)) = prep (Not (E (Not (A v))))
+  | prep (A (Closed v)) = prep (Not (E (Not (Closed v))))
+  | prep (A (NClosed v)) = prep (Not (E (Not (NClosed v))))
+  | prep (Not (Not p)) = prep p
+  | prep (Not (And (p, q))) = Or (prep (Not p), prep (Not q))
+  | prep (Not (A p)) = prep (E (Not p))
+  | prep (Not (Or (p, q))) = And (prep (Not p), prep (Not q))
+  | prep (Not (Imp (p, q))) = And (prep p, prep (Not q))
+  | prep (Not (Iff (p, q))) = Or (prep (And (p, Not q)), prep (And (Not p, q)))
+  | prep (Not T) = Not (prep T)
+  | prep (Not F) = Not (prep F)
+  | prep (Not (Lt v)) = Not (prep (Lt v))
+  | prep (Not (Le v)) = Not (prep (Le v))
+  | prep (Not (Gt v)) = Not (prep (Gt v))
+  | prep (Not (Ge v)) = Not (prep (Ge v))
+  | prep (Not (Eq v)) = Not (prep (Eq v))
+  | prep (Not (NEq v)) = Not (prep (NEq v))
+  | prep (Not (Dvd (v, va))) = Not (prep (Dvd (v, va)))
+  | prep (Not (NDvd (v, va))) = Not (prep (NDvd (v, va)))
+  | prep (Not (E v)) = Not (prep (E v))
+  | prep (Not (Closed v)) = Not (prep (Closed v))
+  | prep (Not (NClosed v)) = Not (prep (NClosed v))
   | prep (Or (p, q)) = Or (prep p, prep q)
   | prep (And (p, q)) = And (prep p, prep q)
-  | prep (Imp (p, q)) = prep (Or (NOT p, q))
-  | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (NOT p, NOT q)))
+  | prep (Imp (p, q)) = prep (Or (Not p, q))
+  | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (Not p, Not q)))
   | prep T = T
   | prep F = F
   | prep (Lt v) = Lt v
--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Oct 18 18:33:46 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 (SOME 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
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -86,21 +86,17 @@
     (qconst_data Morphism.identity, lthy'')
   end
 
-fun mk_readable_rsp_thm_eq tm lthy =
+fun mk_readable_rsp_thm_eq tm ctxt =
   let
-    val ctm = Thm.cterm_of lthy tm
+    val ctm = Thm.cterm_of ctxt tm
 
-    fun norm_fun_eq ctm =
-      let
-        fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
-        fun erase_quants ctm' =
-          case (Thm.term_of ctm') of
-            Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
-            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
-              Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
-      in
-        (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
-      end
+    fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
+    fun erase_quants ctxt' ctm' =
+      case (Thm.term_of ctm') of
+        Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
+        | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+          Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+    val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
 
     fun simp_arrows_conv ctm =
       let
@@ -117,15 +113,15 @@
       end
 
     val unfold_ret_val_invs = Conv.bottom_conv
-      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
+      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt
     val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
-    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt
     val beta_conv = Thm.beta_conversion true
     val eq_thm =
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
-    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
+    Object_Logic.rulify ctxt (eq_thm RS Drule.equal_elim_rule2)
   end
 
 
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Oct 18 18:33:46 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
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Oct 18 18:33:46 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
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Oct 18 18:33:46 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 NONE ct
+        let val (cv, cu) = Thm.dest_abs_global ct
         in add_apps f (Thm.term_of cv :: vs) cu end
     | _ => I)
 
--- a/src/HOL/Tools/SMT/smt_util.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Mon Oct 18 18:33:46 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 (SOME 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)
 
--- a/src/HOL/Tools/SMT/z3_isar.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Mon Oct 18 18:33:46 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 =
--- a/src/HOL/Tools/groebner.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Mon Oct 18 18:33:46 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 NONE (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 (SOME (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
--- a/src/HOL/Tools/record.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/record.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -1355,7 +1355,8 @@
                   (Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, eq), \<^term>\<open>True\<close>));
             in
               SOME (Goal.prove_sorry_global thy [] [] prop
-                (fn _ => simp_tac (put_simpset (get_simpset thy) ctxt
+                (fn {context = ctxt', ...} =>
+                  simp_tac (put_simpset (get_simpset thy) ctxt'
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
             end handle TERM _ => NONE)
         | _ => NONE)
@@ -1602,12 +1603,12 @@
     val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
       simplify (put_simpset HOL_ss defs_ctxt)
         (Goal.prove_sorry_global defs_thy [] [] inject_prop
-          (fn {context = ctxt, ...} =>
-            simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
+          (fn {context = ctxt', ...} =>
+            simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [ext_def]) 1 THEN
             REPEAT_DETERM
-              (resolve_tac ctxt @{thms refl_conj_eq} 1 ORELSE
-                Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
-                resolve_tac ctxt [refl] 1))));
+              (resolve_tac ctxt' @{thms refl_conj_eq} 1 ORELSE
+                Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
+                resolve_tac ctxt' [refl] 1))));
 
 
     (*We need a surjection property r = (| f = f r, g = g r ... |)
@@ -1634,21 +1635,21 @@
 
     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
-        (fn {context = ctxt, ...} =>
+        (fn {context = ctxt', ...} =>
           EVERY1
-           [resolve_tac ctxt @{thms equal_intr_rule},
-            Goal.norm_hhf_tac ctxt,
-            eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt,
-            resolve_tac ctxt [@{thm prop_subst} OF [surject]],
-            REPEAT o eresolve_tac ctxt @{thms meta_allE}, assume_tac ctxt]));
+           [resolve_tac ctxt' @{thms equal_intr_rule},
+            Goal.norm_hhf_tac ctxt',
+            eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
+            resolve_tac ctxt' [@{thm prop_subst} OF [surject]],
+            REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
 
     val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
       let val (assm, concl) = induct_prop in
         Goal.prove_sorry_global defs_thy [] [assm] concl
-          (fn {context = ctxt, prems, ...} =>
+          (fn {context = ctxt', prems, ...} =>
             cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
-            resolve_tac ctxt prems 2 THEN
-            asm_simp_tac (put_simpset HOL_ss ctxt) 1)
+            resolve_tac ctxt' prems 2 THEN
+            asm_simp_tac (put_simpset HOL_ss ctxt') 1)
       end);
 
     val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
@@ -2118,15 +2119,16 @@
     (* 3rd stage: thms_thy *)
 
     val record_ss = get_simpset defs_thy;
-    val sel_upd_ctxt =
-      put_simpset record_ss defs_ctxt
+    fun sel_upd_ctxt ctxt' =
+      put_simpset record_ss ctxt'
         addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
 
     val (sel_convs, upd_convs) =
       timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () =>
         grouped 10 Par_List.map (fn prop =>
             Goal.prove_sorry_global defs_thy [] [] prop
-              (fn _ => ALLGOALS (asm_full_simp_tac sel_upd_ctxt)))
+              (fn {context = ctxt', ...} =>
+                ALLGOALS (asm_full_simp_tac (sel_upd_ctxt ctxt'))))
           (sel_conv_props @ upd_conv_props))
       |> chop (length sel_conv_props);
 
@@ -2141,43 +2143,43 @@
 
     val induct_scheme = timeit_msg defs_ctxt "record induct_scheme proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
-        (fn {context = ctxt, ...} =>
+        (fn {context = ctxt', ...} =>
           EVERY
-           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt rN ind 1,
-            try_param_tac ctxt rN ext_induct 1,
-            asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1]));
+           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt' rN ind 1,
+            try_param_tac ctxt' rN ext_induct 1,
+            asm_simp_tac (put_simpset HOL_basic_ss ctxt') 1]));
 
     val induct = timeit_msg defs_ctxt "record induct proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
-        (fn {context = ctxt, prems, ...} =>
-          try_param_tac ctxt rN induct_scheme 1
-          THEN try_param_tac ctxt "more" @{thm unit.induct} 1
-          THEN resolve_tac ctxt prems 1));
+        (fn {context = ctxt', prems, ...} =>
+          try_param_tac ctxt' rN induct_scheme 1
+          THEN try_param_tac ctxt' "more" @{thm unit.induct} 1
+          THEN resolve_tac ctxt' prems 1));
 
     val surjective = timeit_msg defs_ctxt "record surjective proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] surjective_prop
-        (fn {context = ctxt, ...} =>
+        (fn {context = ctxt', ...} =>
           EVERY
-           [resolve_tac ctxt [surject_assist_idE] 1,
-            simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
+           [resolve_tac ctxt' [surject_assist_idE] 1,
+            simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ext_defs) 1,
             REPEAT
-              (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
-                (resolve_tac ctxt [surject_assistI] 1 THEN
-                  simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
+              (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
+                (resolve_tac ctxt' [surject_assistI] 1 THEN
+                  simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt'
                     addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
 
     val cases_scheme = timeit_msg defs_ctxt "record cases_scheme proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
-        (fn {context = ctxt, prems, ...} =>
-          resolve_tac ctxt prems 1 THEN
-          resolve_tac ctxt [surjective] 1));
+        (fn {context = ctxt', prems, ...} =>
+          resolve_tac ctxt' prems 1 THEN
+          resolve_tac ctxt' [surjective] 1));
 
     val cases = timeit_msg defs_ctxt "record cases proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] cases_prop
-        (fn {context = ctxt, ...} =>
-          try_param_tac ctxt rN cases_scheme 1 THEN
+        (fn {context = ctxt', ...} =>
+          try_param_tac ctxt' rN cases_scheme 1 THEN
           ALLGOALS (asm_full_simp_tac
-            (put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1}))));
+            (put_simpset HOL_basic_ss ctxt' addsimps @{thms unit_all_eq1}))));
 
     val split_meta = timeit_msg defs_ctxt "record split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
@@ -2190,24 +2192,24 @@
 
     val split_object = timeit_msg defs_ctxt "record split_object proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_object_prop
-        (fn {context = ctxt, ...} =>
-          resolve_tac ctxt [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
-          rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
-          resolve_tac ctxt [split_meta] 1));
+        (fn {context = ctxt', ...} =>
+          resolve_tac ctxt' [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
+          rewrite_goals_tac ctxt' @{thms atomize_all [symmetric]} THEN
+          resolve_tac ctxt' [split_meta] 1));
 
     val split_ex = timeit_msg defs_ctxt "record split_ex proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_ex_prop
-        (fn {context = ctxt, ...} =>
+        (fn {context = ctxt', ...} =>
           simp_tac
-            (put_simpset HOL_basic_ss ctxt addsimps
+            (put_simpset HOL_basic_ss ctxt' addsimps
               (@{lemma "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> P x)" by simp} ::
                 @{thms not_not Not_eq_iff})) 1 THEN
-          resolve_tac ctxt [split_object] 1));
+          resolve_tac ctxt' [split_object] 1));
 
     val equality = timeit_msg defs_ctxt "record equality proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] equality_prop
-        (fn {context = ctxt, ...} =>
-          asm_full_simp_tac (put_simpset record_ss ctxt addsimps (split_meta :: sel_convs)) 1));
+        (fn {context = ctxt', ...} =>
+          asm_full_simp_tac (put_simpset record_ss ctxt' addsimps (split_meta :: sel_convs)) 1));
 
     val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
           (_, fold_congs'), (_, unfold_congs'),
--- a/src/HOL/Tools/reification.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/Tools/reification.ML	Mon Oct 18 18:33:46 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,
--- a/src/HOL/ex/Sketch_and_Explore.thy	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Oct 18 18:33:46 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;
--- a/src/Pure/Tools/find_theorems.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Oct 18 18:33:46 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;
 
--- a/src/Pure/conv.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/conv.ML	Mon Oct 18 18:33:46 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 (SOME 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 =
--- a/src/Pure/logic.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/logic.ML	Mon Oct 18 18:33:46 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));
--- a/src/Pure/more_pattern.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/more_pattern.ML	Mon Oct 18 18:33:46 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'')
--- a/src/Pure/more_thm.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Oct 18 18:33:46 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 NONE (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;
--- a/src/Pure/raw_simplifier.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Oct 18 18:33:46 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 (SOME 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 $ _ =>
--- a/src/Pure/term.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/term.ML	Mon Oct 18 18:33:46 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 *)
--- a/src/Pure/thm.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/thm.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -48,7 +48,8 @@
   val dest_arg: cterm -> cterm
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
-  val dest_abs: string option -> 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
@@ -304,12 +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 a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
-      let val (y', t') = Term.dest_abs (the_default x a, 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 _ ct = raise CTERM ("dest_abs", [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]));
+
+val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh;
+val dest_abs_global = gen_dest_abs Term.dest_abs_global;
 
 
 (* constructors *)
--- a/src/Pure/variable.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Pure/variable.ML	Mon Oct 18 18:33:46 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
@@ -313,12 +317,16 @@
 
 (** bounds **)
 
-fun next_bound (a, T) ctxt =
+fun inc_bound (a, T) ctxt =
   let
     val b = Name.bound (#1 (#bounds (rep_data ctxt)));
     val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
   in (Free (b, T), ctxt') end;
 
+fun next_bound a ctxt =
+  let val (x as Free (b, _), ctxt') = inc_bound a ctxt
+  in if Name.is_declared (names_of ctxt') b then inc_bound a ctxt' else (x, ctxt') end;
+
 fun revert_bounds ctxt t =
   (case #2 (#bounds (rep_data ctxt)) of
     [] => t
@@ -326,8 +334,10 @@
       let
         val names = Term.declare_term_names t (names_of ctxt);
         val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
-        fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
-      in Term.subst_atomic (map2 subst bounds xs) t end);
+        fun substs (((b, T), _), x') =
+          let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
+          in [subst T, subst (Type_Annotation.ignore_type T)] end;
+      in Term.subst_atomic (maps substs (bounds ~~ xs)) t end);
 
 
 
@@ -650,6 +660,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);
--- a/src/Tools/Code/code_thingol.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 18 18:33:46 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
--- a/src/Tools/induct.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Tools/induct.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -444,8 +444,8 @@
 val equal_def' = Thm.symmetric Induct_Args.equal_def;
 
 fun mark_constraints n ctxt = Conv.fconv_rule
-  (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
-     (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
+  (Conv.prems_conv ~1 (Conv.params_conv ~1 (fn ctxt' =>
+      Conv.prems_conv n (Raw_Simplifier.rewrite ctxt' false [equal_def'])) ctxt));
 
 fun unmark_constraints ctxt =
   Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
--- a/src/Tools/misc_legacy.ML	Thu Oct 14 16:56:02 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Mon Oct 18 18:33:46 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);