src/HOL/Tools/SMT/smt_normalize.ML

   | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
       Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
   | Const (@{const_name Pure.all}, _) $ Abs _ =>
       Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
   | _ => Conv.all_conv) ct
+  handle CTERM _ => Conv.all_conv ct
 
 val setup_atomize =
   fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
     @{const_name Pure.all}, @{const_name Trueprop}]