--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 20:33:56 2014 +0100
@@ -52,7 +52,7 @@
(case Thm.prop_of thm of
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def (thm RS @{thm fun_cong})
- | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
norm_def (thm RS @{thm meta_eq_to_obj_eq})
| _ => thm)
@@ -61,20 +61,20 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{const "==>"} $ _ $ _ =>
+ @{const Pure.imp} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
- | Const (@{const_name "=="}, _) $ _ $ _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_eq}
- | Const (@{const_name all}, _) $ Abs _ =>
+ | Const (@{const_name Pure.all}, _) $ Abs _ =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
val setup_atomize =
- fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
- @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
+ fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
+ @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
(** unfold special quantifiers **)