# HG changeset patch
# User skalberg
# Date 1064342265 -7200
# Node ID 2fa6ecb87d4725cf5ea6cf0f9cb86c29dfc4cb27
# Parent  97df98601d23556107d0698734b3c7a2bc6aa9ad
Fixed soundness bug.

diff -r 97df98601d23 -r 2fa6ecb87d47 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 23 15:49:17 2003 +0200
+++ b/src/Pure/theory.ML	Tue Sep 23 20:37:45 2003 +0200
@@ -316,7 +316,7 @@
 (* clash_defns *)
 
 fun clash_defn c_ty (name, tm) =
-  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
+  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   end handle TERM _ => None;