src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56245 84fc7dfa3cd4
parent 56107 2ec2d06b9424
child 56981 3ef45ce002b5
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -48,7 +48,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 _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
     1.8 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
     1.9    | _ => thm)
    1.10  
    1.11  
    1.12 @@ -56,17 +56,17 @@
    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 Conv.rewr_conv @{thm atomize_imp}
    1.19 -  | Const (@{const_name "=="}, _) $ _ $ _ =>
    1.20 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
    1.21        Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
    1.22 -  | Const (@{const_name all}, _) $ Abs _ =>
    1.23 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
    1.24        Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
    1.25    | _ => Conv.all_conv) ct
    1.26  
    1.27  val setup_atomize =
    1.28 -  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    1.29 -    @{const_name all}, @{const_name Trueprop}]
    1.30 +  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
    1.31 +    @{const_name Pure.all}, @{const_name Trueprop}]
    1.32  
    1.33  
    1.34  (** unfold special quantifiers **)