src/FOL/simpdata.ML
changeset 56245 84fc7dfa3cd4
parent 54998 8601434fa334
child 58838 59203adfc33f
     1.1 --- a/src/FOL/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    error("conclusion must be a =-equality or <->");;
     1.5  
     1.6  fun mk_eq th = case concl_of th of
     1.7 -    Const("==",_)$_$_           => th
     1.8 +    Const(@{const_name Pure.eq},_)$_$_ => th
     1.9    | _ $ (Const(@{const_name eq},_)$_$_)   => mk_meta_eq th
    1.10    | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
    1.11    | _ $ (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}