src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39315 27f7b7748425
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -408,7 +408,7 @@
     1.4     (@{const_name True}, 0),
     1.5     (@{const_name All}, 1),
     1.6     (@{const_name Ex}, 1),
     1.7 -   (@{const_name "op ="}, 1),
     1.8 +   (@{const_name HOL.eq}, 1),
     1.9     (@{const_name HOL.conj}, 2),
    1.10     (@{const_name HOL.disj}, 2),
    1.11     (@{const_name HOL.implies}, 2),
    1.12 @@ -1275,7 +1275,7 @@
    1.13          forall is_Var args andalso not (has_duplicates (op =) args)
    1.14        | _ => false
    1.15      fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
    1.16 -      | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
    1.17 +      | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
    1.18          do_lhs t1
    1.19        | do_eq _ = false
    1.20    in do_eq end
    1.21 @@ -1347,7 +1347,7 @@
    1.22      @{const "==>"} $ _ $ t2 => term_under_def t2
    1.23    | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
    1.24    | @{const Trueprop} $ t1 => term_under_def t1
    1.25 -  | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
    1.26 +  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
    1.27    | Abs (_, _, t') => term_under_def t'
    1.28    | t1 $ _ => term_under_def t1
    1.29    | _ => t
    1.30 @@ -1371,7 +1371,7 @@
    1.31      val (lhs, rhs) =
    1.32        case t of
    1.33          Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
    1.34 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
    1.35 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
    1.36          (t1, t2)
    1.37        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    1.38      val args = strip_comb lhs |> snd
    1.39 @@ -1453,7 +1453,7 @@
    1.40    | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
    1.41    | @{const Trueprop} $ t1 => lhs_of_equation t1
    1.42    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
    1.43 -  | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
    1.44 +  | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
    1.45    | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
    1.46    | _ => NONE
    1.47  fun is_constr_pattern _ (Bound _) = true
    1.48 @@ -1807,7 +1807,7 @@
    1.49                          (betapply (t2, var_t))
    1.50      end
    1.51    | extensional_equal _ T t1 t2 =
    1.52 -    Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
    1.53 +    Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
    1.54  
    1.55  fun equationalize_term ctxt tag t =
    1.56    let
    1.57 @@ -1816,7 +1816,7 @@
    1.58    in
    1.59      Logic.list_implies (prems,
    1.60          case concl of
    1.61 -          @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
    1.62 +          @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    1.63                                 $ t1 $ t2) =>
    1.64            @{const Trueprop} $ extensional_equal j T t1 t2
    1.65          | @{const Trueprop} $ t' =>
    1.66 @@ -2290,7 +2290,7 @@
    1.67    | simps => simps
    1.68  fun is_equational_fun_surely_complete hol_ctxt x =
    1.69    case equational_fun_axioms hol_ctxt x of
    1.70 -    [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
    1.71 +    [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
    1.72      strip_comb t1 |> snd |> forall is_Var
    1.73    | _ => false
    1.74