src/HOL/Library/Sum_of_Squares/positivstellensatz.ML

 
 fun find_cterm p t =
   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);
 
 fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))

     val strip_exists =
       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
     fun name_of x =
       case Thm.term_of x of

     val strip_forall =
       let
         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
 
     fun f ct =