src/HOL/Statespace/distinct_tree_prover.ML
changeset 29064 70a61d58460e
parent 26343 0dd2eab7b296
child 29269 5c25a2012975
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 10 06:34:10 2008 -0800
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 10 22:55:15 2008 +0100
     1.3 @@ -361,7 +361,7 @@
     1.4                  | NONE => fn i => no_tac)
     1.5  
     1.6  fun distinct_simproc names =
     1.7 -  Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"]
     1.8 +  Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
     1.9      (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
    1.10          case #context (#1 (rep_ss ss)) of
    1.11          SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])