src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39343 eac5f82eefb6
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4                  val t1 = incr_boundvars n t1
     1.5                  val t2 = incr_boundvars n t2
     1.6                  val xs = map Bound (n - 1 downto 0)
     1.7 -                val equation = Const (@{const_name "op ="},
     1.8 +                val equation = Const (@{const_name HOL.eq},
     1.9                                        body_T --> body_T --> bool_T)
    1.10                                     $ betapplys (t1, xs) $ betapplys (t2, xs)
    1.11                  val t =
    1.12 @@ -515,9 +515,9 @@
    1.13            do_description_operator The @{const_name undefined_fast_The} x t1
    1.14          | (Const (x as (@{const_name Eps}, _)), [t1]) =>
    1.15            do_description_operator Eps @{const_name undefined_fast_Eps} x t1
    1.16 -        | (Const (@{const_name "op ="}, T), [t1]) =>
    1.17 +        | (Const (@{const_name HOL.eq}, T), [t1]) =>
    1.18            Op1 (SingletonSet, range_type T, Any, sub t1)
    1.19 -        | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
    1.20 +        | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
    1.21          | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
    1.22            Op2 (And, bool_T, Any, sub' t1, sub' t2)
    1.23          | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>