src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39316 b6c4385ab400
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4    | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
     1.5    | fin_fun_body dom_T ran_T
     1.6                   ((t0 as Const (@{const_name If}, _))
     1.7 -                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
     1.8 +                  $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
     1.9                    $ t2 $ t3) =
    1.10      (if loose_bvar1 (t1', 0) then
    1.11         NONE
    1.12 @@ -650,7 +650,7 @@
    1.13                                       Bound 0)))) accum
    1.14                    |>> mtype_of_mterm
    1.15                  end
    1.16 -              | @{const_name "op ="} => do_equals T accum
    1.17 +              | @{const_name HOL.eq} => do_equals T accum
    1.18                | @{const_name The} =>
    1.19                  (trace_msg (K "*** The"); raise UNSOLVABLE ())
    1.20                | @{const_name Eps} =>
    1.21 @@ -760,7 +760,7 @@
    1.22                      do_term (incr_boundvars ~1 t1') accum
    1.23                    else
    1.24                      raise SAME ()
    1.25 -                | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
    1.26 +                | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
    1.27                    if not (loose_bvar1 (t13, 0)) then
    1.28                      do_term (incr_boundvars ~1 (t11 $ t13)) accum
    1.29                    else
    1.30 @@ -876,7 +876,7 @@
    1.31                  do_term (@{const Not}
    1.32                           $ (HOLogic.eq_const (domain_type T0) $ t1
    1.33                              $ Abs (Name.uu, T1, @{const False}))) accum)
    1.34 -           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.35 +           | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.36               do_equals x t1 t2
    1.37             | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.38               do_formula sn (betapply (t2, t1)) accum
    1.39 @@ -973,7 +973,7 @@
    1.40              do_conjunction t0 t1 t2 accum
    1.41            | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
    1.42              do_all t0 s0 T1 t1 accum
    1.43 -          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.44 +          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.45              consider_general_equals mdata true x t1 t2 accum
    1.46            | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
    1.47            | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.48 @@ -1069,7 +1069,7 @@
    1.49                      Abs (Name.uu, set_T', @{const True})
    1.50                    | _ => Const (s, T')
    1.51                  else if s = @{const_name "=="} orelse
    1.52 -                        s = @{const_name "op ="} then
    1.53 +                        s = @{const_name HOL.eq} then
    1.54                    let
    1.55                      val T =
    1.56                        case T' of