src/HOL/Tools/SMT/smt_normalize.ML
changeset 61033 fd7fe96ca7b9
parent 60642 48dd1cefb4ae
child 61268 abe08fb15a12
     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},