src/HOL/Tools/SMT/smt_normalize.ML
changeset 56245 84fc7dfa3cd4
parent 55414 eab03e9cee8a
child 57996 ca917ea6969c
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4    (case Thm.prop_of thm of
     1.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
     1.6        norm_def (thm RS @{thm fun_cong})
     1.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
     1.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
     1.9        norm_def (thm RS @{thm meta_eq_to_obj_eq})
    1.10    | _ => thm)
    1.11  
    1.12 @@ -61,20 +61,20 @@
    1.13  
    1.14  fun atomize_conv ctxt ct =
    1.15    (case Thm.term_of ct of
    1.16 -    @{const "==>"} $ _ $ _ =>
    1.17 +    @{const Pure.imp} $ _ $ _ =>
    1.18        Conv.binop_conv (atomize_conv ctxt) then_conv
    1.19        Conv.rewr_conv @{thm atomize_imp}
    1.20 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
    1.21 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
    1.22        Conv.binop_conv (atomize_conv ctxt) then_conv
    1.23        Conv.rewr_conv @{thm atomize_eq}
    1.24 -  | Const (@{const_name all}, _) $ Abs _ =>
    1.25 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
    1.26        Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    1.27        Conv.rewr_conv @{thm atomize_all}
    1.28    | _ => Conv.all_conv) ct
    1.29  
    1.30  val setup_atomize =
    1.31 -  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    1.32 -    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    1.33 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
    1.34 +    @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
    1.35  
    1.36  
    1.37  (** unfold special quantifiers **)