1.1 --- a/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4                  | NONE => fn i => no_tac)
     1.5  
     1.6  val distinct_simproc =
     1.7 -  Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
     1.8 +  Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
     1.9      (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
    1.10          (case try Simplifier.the_context ss of
    1.11            SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])