generate proper error instead of exception if goal cannot be atomized
authorblanchet
Thu Aug 27 22:36:09 2015 +0200 (2015-08-27)
changeset 61033fd7fe96ca7b9
parent 61032 b57df8eecad6
child 61035 5fa9962e6c38
generate proper error instead of exception if goal cannot be atomized
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 27 21:19:48 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 27 22:36:09 2015 +0200
     1.3 @@ -68,6 +68,7 @@
     1.4    | Const (@{const_name Pure.all}, _) $ Abs _ =>
     1.5        Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
     1.6    | _ => Conv.all_conv) ct
     1.7 +  handle CTERM _ => Conv.all_conv ct
     1.8  
     1.9  val setup_atomize =
    1.10    fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
     2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 21:19:48 2015 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Aug 27 22:36:09 2015 +0200
     2.3 @@ -257,7 +257,7 @@
     2.4      val cprop =
     2.5        (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of
     2.6          SOME ct => ct
     2.7 -      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "goal is not a HOL term"))
     2.8 +      | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal"))
     2.9  
    2.10      val conjecture = Thm.assume cprop
    2.11      val facts = map snd xfacts