src/HOL/Statespace/state_space.ML
changeset 38549 d0385f2764d8
parent 38389 d7d915bae307
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Statespace/state_space.ML	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -222,8 +222,8 @@
     1.4    end handle Option => NONE)
     1.5  
     1.6  fun distinctTree_tac ctxt
     1.7 -      (Const ("Trueprop",_) $
     1.8 -        (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
     1.9 +      (Const (@{const_name "Trueprop"},_) $
    1.10 +        (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
    1.11    (case (neq_x_y ctxt x y) of
    1.12       SOME neq => rtac neq i
    1.13     | NONE => no_tac)
    1.14 @@ -236,7 +236,7 @@
    1.15  
    1.16  val distinct_simproc =
    1.17    Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    1.18 -    (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
    1.19 +    (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
    1.20          (case try Simplifier.the_context ss of
    1.21            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
    1.22                         (neq_x_y ctxt x y)