src/HOL/Tools/SMT/smt_solver.ML

       |> Config.put SMT_Config.filter_only_facts true
 
     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
     |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
     |> tap check_topsort