clarified signature;

--- a/src/HOL/Analysis/metric_arith.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -92,7 +92,7 @@
           app_union_ct_pair find (Thm.dest_comb ct)
         | Abs (_, _, _) =>
           (* ensure the point doesn't contain the bound variable *)
-          let val (var, bod) = Thm.dest_abs NONE ct in
+          let val (var, bod) = Thm.dest_abs ct in
             filter (free_in var #> not) (find bod)
           end
         | _ => [])
@@ -120,7 +120,7 @@
       | _ $ _ =>
         app_union_ct_pair find (Thm.dest_comb ct)
       | Abs (_, _, _) =>
-        let val (var, bod) = Thm.dest_abs NONE ct in
+        let val (var, bod) = Thm.dest_abs ct in
           filter (free_in var #> not) (find bod)
         end
       | _ => []
@@ -139,7 +139,7 @@
           else app_union_ct_pair find (Thm.dest_binop ct)
       | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
       | Abs (_, _, _) =>
-        let val (var, bod) = Thm.dest_abs NONE ct in
+        let val (var, bod) = Thm.dest_abs ct in
           filter (free_in var #> not) (find bod)
         end
       | _ => []
@@ -255,7 +255,7 @@
       let val (s, t) = Thm.dest_comb ct in
         default (find_dist t) (find_dist s)
       end
-    | Abs (_, _, _) => find_dist (snd (Thm.dest_abs NONE ct))
+    | Abs (_, _, _) => find_dist (snd (Thm.dest_abs ct))
     | _ => NONE
   fun find_eq ct =
     case Thm.term_of ct of
@@ -269,7 +269,7 @@
       let val (s, t) = Thm.dest_comb ct in
         default (find_eq t) (find_eq s)
       end
-    | Abs (_, _, _) => find_eq (snd (Thm.dest_abs NONE ct))
+    | Abs (_, _, _) => find_eq (snd (Thm.dest_abs ct))
     | _ => NONE
   in
     case default (find_eq ct) (find_dist ct) of

--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -24,7 +24,7 @@
                  simpset : simpset};
 
 fun get_p1 th =
-  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
     (funpow 2 Thm.dest_arg (Thm.cprop_of th)) |> Thm.dest_arg
 
 fun ferrack_conv ctxt
@@ -55,7 +55,7 @@
     in (S,th) end
 
  val ((p1_v,p2_v),(mp1_v,mp2_v)) =
-   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
+   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs)
      (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
    |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
    |> apply2 (apply2 (dest_Var o Thm.term_of))
@@ -79,7 +79,7 @@
   let
    val ((xn,ce),(x,fm)) = (case Thm.term_of p of
                    \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> =>
-                        Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
+                        Thm.dest_comb p ||> Thm.dest_abs_name xn |>> pair xn
                  | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    val cT = Thm.ctyp_of_cterm x
    val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
@@ -191,7 +191,7 @@
   and find_args bounds tm =
            (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
  and find_body bounds b =
-   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+   let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
    in h (bounds + 1) b' end;
 in h end;
 

--- a/src/HOL/Decision_Procs/langford.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -41,7 +41,7 @@
           simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
             (Thm.instantiate' [] [SOME p] stupid)
         val (L, U) =
-          let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
+          let val (_, q) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of ths))
           in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
         fun proveneF S =
           let
@@ -131,7 +131,7 @@
     \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
       let
         val e = Thm.dest_fun ct
-        val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
+        val (x,p) = Thm.dest_abs_name xn (Thm.dest_arg ct)
         val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p
         val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
       in
@@ -210,7 +210,7 @@
     and find_args bounds tm =
       (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
     and find_body bounds b =
-      let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+      let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
       in h (bounds + 1) b' end;
   in h end;
 
@@ -240,7 +240,7 @@
           then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
           else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
       | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-      | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+      | Abs _ => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
       | Free _ => if member (op aconvc) ats t then acc else ins t acc
       | Var _ => if member (op aconvc) ats t then acc else ins t acc
       | _ => acc)

--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -308,7 +308,7 @@
   if p t then t else
   case Thm.term_of t of
     _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
-  | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
+  | Abs (_,_,_) => find_cterm p (Thm.dest_abs t |> snd)
   | _ => raise CTERM ("find_cterm",[t]);
 
 fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
@@ -496,7 +496,7 @@
         fun h (acc, t) =
           case Thm.term_of t of
             Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
-              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+              h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
       end
@@ -541,7 +541,7 @@
         fun h (acc, t) =
           case Thm.term_of t of
             Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
-              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+              h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
           | _ => (acc,t)
       in fn t => h ([],t)
       end

--- a/src/HOL/Library/cconv.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Library/cconv.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -153,7 +153,7 @@
 
          (* Destruct the abstraction and apply the conversion. *)
          val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
-         val (v, ct') = Thm.dest_abs (SOME u) ct
+         val (v, ct') = Thm.dest_abs_name u ct
          val eq = cv (v, ctxt') ct'
        in
          if Thm.is_reflexive eq

--- a/src/HOL/Library/old_recdef.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -110,7 +110,7 @@
 signature DCTERM =
 sig
   val dest_comb: cterm -> cterm * cterm
-  val dest_abs: string option -> cterm -> cterm * cterm
+  val dest_abs: cterm -> cterm * cterm
   val capply: cterm -> cterm -> cterm
   val cabs: cterm -> cterm -> cterm
   val mk_conj: cterm * cterm -> cterm
@@ -774,7 +774,7 @@
 fun dest_comb t = Thm.dest_comb t
   handle CTERM (msg, _) => raise ERR "dest_comb" msg;
 
-fun dest_abs a t = Thm.dest_abs a t
+fun dest_abs t = Thm.dest_abs t
   handle CTERM (msg, _) => raise ERR "dest_abs" msg;
 
 fun capply t u = Thm.apply t u
@@ -838,7 +838,7 @@
  in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
 
 fun dest_binder expected tm =
-  dest_abs NONE (dest_monop expected tm)
+  dest_abs (dest_monop expected tm)
   handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
 
 
@@ -883,7 +883,7 @@
 
 val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
 val strip_imp    = rev2swap o strip dest_imp
-val strip_abs    = rev2swap o strip (dest_abs NONE)
+val strip_abs    = rev2swap o strip dest_abs
 val strip_forall = rev2swap o strip dest_forall
 val strip_exists = rev2swap o strip dest_exists
 

--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -165,7 +165,7 @@
     fun rewrite_subterm prems ct (Abs (x, _, _)) =
       let
         val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt;
-        val (v, ct') = Thm.dest_abs (SOME u) ct;
+        val (v, ct') = Thm.dest_abs_name u ct;
         val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct'
       in
         if Thm.is_reflexive thm then

--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -90,7 +90,7 @@
 fun abstract ctxt ct =
   let
       val Abs (_, _, body) = Thm.term_of ct
-      val (x, cbody) = Thm.dest_abs NONE ct
+      val (x, cbody) = Thm.dest_abs ct
       val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
       fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
   in
@@ -142,7 +142,7 @@
   else case Thm.term_of ct of
     Abs _ =>
     let
-      val (cv, cta) = Thm.dest_abs NONE ct
+      val (cv, cta) = Thm.dest_abs ct
       val (v, _) = dest_Free (Thm.term_of cv)
       val u_th = introduce_combinators_in_cterm ctxt cta
       val cu = Thm.rhs_of u_th
@@ -174,7 +174,7 @@
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
 fun c_variant_abs_multi (ct0, vars) =
-      let val (cv,ct) = Thm.dest_abs NONE ct0
+      let val (cv,ct) = Thm.dest_abs ct0
       in  c_variant_abs_multi (ct, cv::vars)  end
       handle CTERM _ => (ct0, rev vars);
 
@@ -266,7 +266,7 @@
         Const (s, _) $ Abs (s', _, _) =>
         if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
            s = \<^const_name>\<open>Ex\<close> then
-          Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
+          Thm.dest_comb #> snd #> Thm.dest_abs_name s' #> snd #> zap pos
         else
           Conv.all_conv
       | Const (s, _) $ _ $ _ =>

--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -145,7 +145,7 @@
 
 fun get_pmi_term t =
   let val (x,eq) =
-     (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
+     (Thm.dest_abs o Thm.dest_arg o snd o Thm.dest_abs o Thm.dest_arg)
         (Thm.dest_arg t)
 in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
 
@@ -348,7 +348,7 @@
 
 fun unify ctxt q =
  let
-  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
+  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs
   val x = Thm.term_of cx
   val ins = insert (op = : int * int -> bool)
   fun h (acc,dacc) t =
@@ -436,8 +436,8 @@
 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
 val [A_v,B_v] =
   map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
-    |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
-    |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg
+    |> Thm.dest_abs |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+    |> Thm.dest_abs |> snd |> Thm.dest_fun |> Thm.dest_arg
     |> Thm.term_of |> dest_Var) [asetP, bsetP];
 
 val D_v = (("D", 0), \<^typ>\<open>int\<close>);
@@ -446,7 +446,7 @@
 let
 
  val uth = unify ctxt q
- val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
+ val (x,p) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of uth))
  val ins = insert (op aconvc)
  fun h t (bacc,aacc,dacc) =
   case (whatis x t) of
@@ -717,7 +717,7 @@
 fun strip_objall ct =
  case Thm.term_of ct of
   Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) =>
-   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
+   let val (a,(v,t')) = (apsnd (Thm.dest_abs_name xn) o Thm.dest_comb) ct
    in apfst (cons (a,v)) (strip_objall t')
    end
 | _ => ([],ct);
@@ -798,7 +798,7 @@
   fun h acc t = if ty cts t then insert (op aconvc) t acc else
    case Thm.term_of t of
     _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+  | Abs(_,_,_) => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc))
   | _ => acc
  in h [] ct end
 end;

--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -32,7 +32,7 @@
   | Const(\<^const_name>\<open>Ex\<close>,_)$Abs(s,_,_) =>
     let
      val (e,p0) = Thm.dest_comb p
-     val (x,p') = Thm.dest_abs (SOME s) p0
+     val (x,p') = Thm.dest_abs_name s p0
      val env' = ins x env
      val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
                    |> Drule.arg_cong_rule e

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -382,7 +382,7 @@
         let val (cu1, cu2) = Thm.dest_comb ct
         in f vs cu1 cu2 #> add_apps f vs cu1 #> add_apps f vs cu2 end
     | Abs _ =>
-        let val (cv, cu) = Thm.dest_abs NONE ct
+        let val (cv, cu) = Thm.dest_abs ct
         in add_apps f (Thm.term_of cv :: vs) cu end
     | _ => I)
 

--- a/src/HOL/Tools/SMT/smt_util.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -185,7 +185,7 @@
   (case Thm.term_of ct of
     Abs _ =>
       let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
-      in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
+      in (snd (Thm.dest_abs_name n ct), ctxt') end
   | _ => raise CTERM ("no abstraction", [ct]))
 
 val dest_all_cabs = repeat_yield (try o dest_cabs)

--- a/src/HOL/Tools/groebner.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -386,7 +386,7 @@
  let fun h (acc, t) =
       case Thm.term_of t of
        Const (\<^const_name>\<open>Ex\<close>, _) $ Abs _ =>
-        h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+        h (Thm.dest_abs (Thm.dest_arg t) |>> (fn v => v::acc))
      | _ => (acc,t)
  in fn t => h ([],t)
  end;
@@ -904,7 +904,7 @@
   let val (t, u) = Thm.dest_binop tm
   in (find_term bounds t handle TERM _ => find_term bounds u) end
 and find_body bounds b =
-  let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+  let val (_, b') = Thm.dest_abs_name (Name.bound bounds) b
   in find_term (bounds + 1) b' end;
 
 

--- a/src/Pure/conv.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/Pure/conv.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -94,7 +94,7 @@
     Abs (x, _, _) =>
       let
         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
-        val (v, ct') = Thm.dest_abs (SOME u) ct;
+        val (v, ct') = Thm.dest_abs_name u ct;
         val eq = cv (v, ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));

--- a/src/Pure/more_thm.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -339,7 +339,7 @@
 fun dest_all ct =
   (case Thm.term_of ct of
     Const ("Pure.all", _) $ Abs (a, _, _) =>
-      let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct)
+      let val (x, ct') = Thm.dest_abs (Thm.dest_arg ct)
       in SOME ((a, Thm.ctyp_of_cterm x), ct') end
   | _ => NONE);
 

--- a/src/Pure/raw_simplifier.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -1134,7 +1134,7 @@
                 let
                     val (v, ctxt') = Variable.next_bound (a, T) ctxt;
                     val b = #1 (Term.dest_Free v);
-                    val (v', t') = Thm.dest_abs (SOME b) t0;
+                    val (v', t') = Thm.dest_abs_name b t0;
                     val b' = #1 (Term.dest_Free (Thm.term_of v'));
                     val _ =
                       if b <> b' then

--- a/src/Pure/thm.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/Pure/thm.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -48,7 +48,8 @@
   val dest_arg: cterm -> cterm
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
-  val dest_abs: string option -> cterm -> cterm * cterm
+  val dest_abs_name: string -> cterm -> cterm * cterm
+  val dest_abs: cterm -> cterm * cterm
   val rename_tvar: indexname -> ctyp -> ctyp
   val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
@@ -304,12 +305,15 @@
       in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
 
-fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
-      let val (y', t') = Term.dest_abs (the_default x a, T, t) in
+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 _ ct = raise CTERM ("dest_abs", [ct]);
+  | dest_abs_name _ ct = raise CTERM ("dest_abs_name", [ct]);
+
+fun dest_abs (ct as Cterm {t = Abs (x, _, _), ...}) = dest_abs_name x ct
+  | dest_abs ct = raise CTERM ("dest_abs", [ct]);
 
 
 (* constructors *)