src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -335,7 +335,7 @@
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
-      if Logic.is_equals (Thm.concl_of thm) then [thm]
+      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
       else [thm RS reflect] handle THM _ => [];
 
     fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);