src/Pure/variable.ML

--- a/src/Pure/variable.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/variable.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -81,6 +81,10 @@
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
+  val dest_abs: term -> Proof.context -> ((string * typ) * term) * Proof.context
+  val dest_abs_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
+  val dest_all: term -> Proof.context -> ((string * typ) * term) * Proof.context
+  val dest_all_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context
   val is_bound_focus: Proof.context -> bool
   val set_bound_focus: bool -> Proof.context -> Proof.context
   val restore_bound_focus: Proof.context -> Proof.context -> Proof.context
@@ -650,6 +654,40 @@
 val trade = gen_trade (import true) export;
 
 
+(* destruct binders *)
+
+local
+
+fun gen_dest_abs exn dest term_of arg ctxt =
+  (case term_of arg of
+    Abs (a, T, _) =>
+      let
+        val (x, ctxt') = yield_singleton bound_fixes (a, T) ctxt;
+        val res = dest x arg handle Term.USED_FREE _ =>
+          raise Fail ("Bad context: clash of fresh free for bound: " ^
+            Syntax.string_of_term ctxt (Free (x, T)) ^ " vs. " ^
+            Syntax.string_of_term ctxt' (Free (x, T)));
+      in (res, ctxt') end
+  | _ => raise exn ("dest_abs", [arg]));
+
+in
+
+val dest_abs = gen_dest_abs TERM Term.dest_abs_fresh I;
+val dest_abs_cterm = gen_dest_abs CTERM Thm.dest_abs_fresh Thm.term_of;
+
+fun dest_all t ctxt =
+  (case t of
+    Const ("Pure.all", _) $ u => dest_abs u ctxt
+  | _ => raise TERM ("dest_all", [t]));
+
+fun dest_all_cterm ct ctxt =
+  (case Thm.term_of ct of
+    Const ("Pure.all", _) $ _ => dest_abs_cterm (Thm.dest_arg ct) ctxt
+  | _ => raise CTERM ("dest_all", [ct]));
+
+end;
+
+
 (* focus on outermost parameters: \<And>x y z. B *)
 
 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);