--- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Aug 25 18:36:22 2010 +0200
@@ -355,7 +355,7 @@
| NONE => fn i => no_tac)
fun distinct_simproc names =
- Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
+ Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
(fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])