src/HOL/Tools/SMT/smt_solver.ML
changeset 61033 fd7fe96ca7b9
parent 60752 b48830b670a1
child 61268 abe08fb15a12
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 21:19:48 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 22:36:09 2015 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4      val cprop =
     1.5        (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of
     1.6          SOME ct => ct
     1.7 -      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "goal is not a HOL term"))
     1.8 +      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal"))
     1.9  
    1.10      val conjecture = Thm.assume cprop
    1.11      val facts = map snd xfacts