src/Pure/thm.ML

--- a/src/Pure/thm.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/thm.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -48,8 +48,8 @@
   val dest_arg: cterm -> cterm
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
-  val dest_abs_name: string -> cterm -> cterm * cterm
-  val dest_abs: 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
@@ -305,15 +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_name x (Cterm {t = Abs (_, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
-      let val (y', t') = Term.dest_abs (x, 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_name _ ct = raise CTERM ("dest_abs_name", [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]));
 
-fun dest_abs (ct as Cterm {t = Abs (x, _, _), ...}) = dest_abs_name x ct
-  | dest_abs ct = 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 *)