Fixed soundness bug.

--- 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;