src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39345 062c10ff848c
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4      fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
     1.5          aux def t1 andalso aux false t2
     1.6        | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
     1.7 -      | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
     1.8 +      | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
     1.9          aux def t1 andalso aux false t2
    1.10        | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
    1.11        | aux def (t1 $ t2) = aux def t1 andalso aux def t2
    1.12 @@ -149,7 +149,7 @@
    1.13        case t of
    1.14          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
    1.15        | Const (s0, _) $ t1 $ _ =>
    1.16 -        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
    1.17 +        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
    1.18            let
    1.19              val (t', args) = strip_comb t1
    1.20              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
    1.21 @@ -209,7 +209,7 @@
    1.22          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
    1.23        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
    1.24          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
    1.25 -      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
    1.26 +      | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
    1.27          do_equals new_Ts old_Ts s0 T0 t1 t2
    1.28        | @{const HOL.conj} $ t1 $ t2 =>
    1.29          @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
    1.30 @@ -332,7 +332,7 @@
    1.31          do_eq_or_imp Ts true def t0 t1 t2 seen
    1.32        | (t0 as @{const "==>"}) $ t1 $ t2 =>
    1.33          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
    1.34 -      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.35 +      | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.36          do_eq_or_imp Ts true def t0 t1 t2 seen
    1.37        | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
    1.38          do_eq_or_imp Ts false def t0 t1 t2 seen
    1.39 @@ -399,7 +399,7 @@
    1.40          aux_eq careful true t0 t1 t2
    1.41        | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
    1.42          t0 $ aux false t1 $ aux careful t2
    1.43 -      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
    1.44 +      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
    1.45          aux_eq careful true t0 t1 t2
    1.46        | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
    1.47          t0 $ aux false t1 $ aux careful t2
    1.48 @@ -464,9 +464,9 @@
    1.49      and aux_implies prems zs t1 t2 =
    1.50        case t1 of
    1.51          Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
    1.52 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
    1.53 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
    1.54          aux_eq prems zs z t' t1 t2
    1.55 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
    1.56 +      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
    1.57          aux_eq prems zs z t' t1 t2
    1.58        | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
    1.59      and aux_eq prems zs z t' t1 t2 =
    1.60 @@ -499,7 +499,7 @@
    1.61              handle SAME () => do_term (t :: seen) ts
    1.62          in
    1.63            case t of
    1.64 -            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
    1.65 +            Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
    1.66            | _ => do_term (t :: seen) ts
    1.67          end
    1.68    in do_term end
    1.69 @@ -653,7 +653,7 @@
    1.70  
    1.71  fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
    1.72    | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
    1.73 -  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
    1.74 +  | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
    1.75      snd (strip_comb t1)
    1.76    | params_in_equation _ = []
    1.77