src/HOL/Tools/simpdata.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 42364 8c674b3b8e44
     1.1 --- a/src/HOL/Tools/simpdata.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  structure Quantifier1 = Quantifier1Fun
     1.5  (struct
     1.6    (*abstract syntax*)
     1.7 -  fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
     1.8 +  fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
     1.9      | dest_eq _ = NONE;
    1.10    fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
    1.11      | dest_conj _ = NONE;
    1.12 @@ -44,7 +44,7 @@
    1.13  fun mk_eq th = case concl_of th
    1.14    (*expects Trueprop if not == *)
    1.15    of Const (@{const_name "=="},_) $ _ $ _ => th
    1.16 -   | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
    1.17 +   | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
    1.18     | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    1.19     | _ => th RS @{thm Eq_TrueI}
    1.20