src/HOL/Statespace/state_space.ML
changeset 38864 4abe644fcea5
parent 38835 088502dfd89f
child 39134 917b4b6ba3d2
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  
     1.5  fun distinctTree_tac ctxt
     1.6        (Const (@{const_name Trueprop},_) $
     1.7 -        (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
     1.8 +        (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
     1.9    (case (neq_x_y ctxt x y) of
    1.10       SOME neq => rtac neq i
    1.11     | NONE => no_tac)
    1.12 @@ -236,7 +236,7 @@
    1.13  
    1.14  val distinct_simproc =
    1.15    Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    1.16 -    (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
    1.17 +    (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
    1.18          (case try Simplifier.the_context ss of
    1.19            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
    1.20                         (neq_x_y ctxt x y)