src/HOL/Tools/simpdata.ML
changeset 56245 84fc7dfa3cd4
parent 56073 29e308b56d23
child 58839 ccda99401bc8
     1.1 --- a/src/HOL/Tools/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  fun mk_eq th = case concl_of th
     1.6    (*expects Trueprop if not == *)
     1.7 -  of Const (@{const_name "=="},_) $ _ $ _ => th
     1.8 +  of Const (@{const_name Pure.eq},_) $ _ $ _ => th
     1.9     | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
    1.10     | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    1.11     | _ => th RS @{thm Eq_TrueI}