diff -r c86fcf44b4c9 -r c0fa8499e366 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:39 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:40 2010 +0200
@@ -108,13 +108,15 @@
       val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
       val intross4 = map_specs (maps remove_pointless_clauses) intross3
       val _ = print_intross options thy''' "After removing pointless clauses: " intross4
-      val intross5 =
-        map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
-      val intross6 = map_specs (map (expand_tuples thy''')) intross5
-      val intross7 = map_specs (map (eta_contract_ho_arguments thy''')) intross6
-      val _ = print_intross options thy''' "introduction rules before registering: " intross7
+      val intross5 = map_specs (map (remove_equalities thy''')) intross4
+      val _ = print_intross options thy''' "After removing equality premises:" intross5
+      val intross6 =
+        map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross5
+      val intross7 = map_specs (map (expand_tuples thy''')) intross6
+      val intross8 = map_specs (map (eta_contract_ho_arguments thy''')) intross7
+      val _ = print_intross options thy''' "introduction rules before registering: " intross8
       val _ = print_step options "Registering introduction rules..."
-      val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
+      val thy'''' = fold Predicate_Compile_Core.register_intros intross8 thy'''
     in
       thy''''
     end;