# HG changeset patch
# User blanchet
# Date 1440707769 -7200
# Node ID fd7fe96ca7b95213f11cd40a2961a7123c442624
# Parent  b57df8eecad6097a3e01e2ed8c06739b41ec2ab2
generate proper error instead of exception if goal cannot be atomized

diff -r b57df8eecad6 -r fd7fe96ca7b9 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},
diff -r b57df8eecad6 -r fd7fe96ca7b9 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 21:19:48 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 22:36:09 2015 +0200
@@ -257,7 +257,7 @@
     val cprop =
       (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of
         SOME ct => ct
-      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "goal is not a HOL term"))
+      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal"))
 
     val conjecture = Thm.assume cprop
     val facts = map snd xfacts