src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

   val mk_predT: typ list -> typ
   val mk_pred1T: typ -> typ
 
   val mk_disjIN: int -> int -> thm
 
+  val mk_abs_def: thm -> thm
   val mk_unabs_def: int -> thm -> thm
 
   val mk_IfN: typ -> term list -> term list -> term
   val mk_Trueprop_eq: term * term -> term
   val mk_Trueprop_mem: term * term -> term

 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
   | mk_disjIN _ 1 = disjI1
   | mk_disjIN 2 2 = disjI2
   | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
 
+fun mk_abs_def thm = Drule.abs_def (thm RS eq_reflection handle THM _ => thm);
 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
 fun mk_IfN _ _ [t] = t
   | mk_IfN T (c :: cs) (t :: ts) =
     Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;