diff -r 8ee3d5d3c1bf -r c960bfcb91db src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/logic.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -11,7 +11,7 @@
   val all: term -> term -> term
   val dependent_all_name: string * term -> term -> term
   val is_all: term -> bool
-  val dest_all: term -> (string * typ) * term
+  val dest_all_global: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
   val all_constraint: (string -> typ option) -> string * string -> term -> term
   val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
@@ -125,10 +125,10 @@
 fun is_all (Const ("Pure.all", _) $ Abs _) = true
   | is_all _ = false;
 
-fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
-      let val (x, b) = Term.dest_abs abs  (*potentially slow*)
-      in ((x, T), b) end
-  | dest_all t = raise TERM ("dest_all", [t]);
+fun dest_all_global t =
+  (case t of
+    Const ("Pure.all", _) $ (u as Abs _) => Term.dest_abs_global u
+  | _ => raise TERM ("dest_all", [t]));
 
 fun list_all ([], t) = t
   | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));