# HG changeset patch
# User haftmann
# Date 1281628604 -7200
# Node ID 2d6dc3f25686b8b37184f78b501ef09d7f02fe6a
# Parent  3142c1e21a0e25fe46a3bfc718ee593df0612cf6
dropped dead code

diff -r 3142c1e21a0e -r 2d6dc3f25686 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 12 17:56:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 12 17:56:44 2010 +0200
@@ -511,8 +511,6 @@
    clearly inconsistent facts such as X = a | X = b, though it by no means
    guarantees soundness. *)
 
-fun is_record_type T = not (null (Record.dest_recTs T))
-
 (* Unwanted equalities are those between a (bound or schematic) variable that
    does not properly occur in the second operand. *)
 fun too_general_eqterms (Var z) t =