# HG changeset patch
# User boehmes
# Date 1302282248 -7200
# Node ID 1f09e4c680fc6e24ab45d85dbbc073470f01ad15
# Parent  9a8ba59aed06501fc96bf5a240315a71fb98be0d
check if negating the goal is possible (avoids CTERM exception for Pure propositions)

diff -r 9a8ba59aed06 -r 1f09e4c680fc src/HOL/Tools/SMT/smt_solver.ML
--- 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