src/HOL/Tools/SMT/smt_normalize.ML

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 27 21:19:48 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 27 22:36:09 2015 +0200
@@ -68,6 +68,7 @@
   | 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},