check if negating the goal is possible (avoids CTERM exception for Pure propositions)

--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Apr 08 19:04:08 2011 +0200
@@ -284,7 +284,11 @@
     val {facts, goal, ...} = Proof.goal st
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
-    val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
+    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")))
   in
     map snd xwthms
     |> map_index I