src/HOL/Tools/Nitpick/minipick.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4           Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
     1.5         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
     1.6           to_F Ts (t0 $ eta_expand Ts t1 1)
     1.7 -       | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
     1.8 +       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
     1.9           RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
    1.10         | Const (@{const_name ord_class.less_eq},
    1.11                  Type (@{type_name fun},
    1.12 @@ -165,8 +165,8 @@
    1.13           @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
    1.14         | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
    1.15         | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
    1.16 -       | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
    1.17 -       | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
    1.18 +       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
    1.19 +       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
    1.20         | Const (@{const_name ord_class.less_eq},
    1.21                  Type (@{type_name fun},
    1.22                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>