--- 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));