# HG changeset patch
# User wenzelm
# Date 1702205816 -3600
# Node ID e81b7689b26404af4837f67223db74bde1c39917
# Parent  a8db9ee24d5eb0a59ecb90f8d3cd1024fec2ca24
clarified ML;

diff -r a8db9ee24d5e -r e81b7689b264 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Dec 10 11:42:57 2023 +0100
+++ b/src/Pure/term.ML	Sun Dec 10 11:56:56 2023 +0100
@@ -392,29 +392,27 @@
 
 fun abs (x, T) t = Abs (x, T, t);
 
-fun strip_abs (Abs (a, T, t)) =
-      let val (a', t') = strip_abs t
-      in ((a, T) :: a', t') end
+fun strip_abs (Abs (a, T, t)) = strip_abs t |>> cons (a, T)
   | strip_abs t = ([], t);
 
-(*maps  (x1,...,xn)t   to   t*)
-fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
-  | strip_abs_body u  =  u;
+fun strip_abs_body (Abs (_, _, t)) = strip_abs_body t
+  | strip_abs_body t = t;
 
-(*maps  (x1,...,xn)t   to   [x1, ..., xn]*)
-fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
-  | strip_abs_vars u  =  [] : (string*typ) list;
+fun strip_abs_vars (Abs (a, T, t)) = strip_abs_vars t |> cons (a, T)
+  | strip_abs_vars _ = [];
 
 
 fun strip_qnt_body qnt =
-let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
-      | strip t = t
-in strip end;
+  let
+    fun strip (tm as Const (c, _) $ Abs (_, _, t)) = if c = qnt then strip t else tm
+      | strip t = t;
+  in strip end;
 
 fun strip_qnt_vars qnt =
-let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
-      | strip t  =  [] : (string*typ) list
-in strip end;
+  let
+    fun strip (Const (c, _) $ Abs (a, T, t)) = if c = qnt then (a, T) :: strip t else []
+      | strip _ = [];
+  in strip end;
 
 
 (*maps   (f, [t1,...,tn])  to  f(t1,...,tn)*)