src/HOL/Tools/SMT/smt_normalize.ML

     (case Thm.term_of ct of
       _ $ _ =>
         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 ct
+        let val (cv, cu) = Thm.dest_abs_global ct
         in add_apps f (Thm.term_of cv :: vs) cu end
     | _ => I)
 
   val int_thm = @{lemma "(0::int) <= int (n::nat)" by simp}
   val nat_int_thms = @{lemma