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