src/HOL/HOL.thy

         eq $ lhs $ rhs =>
           (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
             SOME thm => SOME (thm RS neq_to_EQ_False)
           | NONE => NONE)
        | _ => NONE);
-  in proc end;
+  in proc end
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
   let
     fun count_loose (Bound i) k = if i >= k then 1 else 0