src/HOL/HOL.thy
changeset 43597 b4a093e755db
parent 43560 d1650e3720fd
child 43654 3f1a44c2d645
     1.1 --- a/src/HOL/HOL.thy	Wed Jun 29 20:39:41 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Jun 29 21:34:16 2011 +0200
     1.3 @@ -1232,7 +1232,7 @@
     1.4    fun proc ss ct =
     1.5      (case Thm.term_of ct of
     1.6        eq $ lhs $ rhs =>
     1.7 -        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of
     1.8 +        (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
     1.9            SOME thm => SOME (thm RS neq_to_EQ_False)
    1.10          | NONE => NONE)
    1.11       | _ => NONE);