src/HOL/Tools/SMT/smt_normalize.ML
changeset 38864 4abe644fcea5
parent 37786 4eb98849c5c0
child 39483 9f0e5684f04b
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4  
     1.5  fun norm_def ctxt thm =
     1.6    (case Thm.prop_of thm of
     1.7 -    @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
     1.8 +    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
     1.9        norm_def ctxt (thm RS @{thm fun_cong})
    1.10    | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    1.11        norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})