# HG changeset patch
# User kuncar
# Date 1392911792 -3600
# Node ID 18da8519936712ae9bdf3b7f70a20af8de366fee
# Parent  332641e48ff49d912845c8f407594fda9e9ce362
the rule is not needed due to 1726f46d2aa8

diff -r 332641e48ff4 -r 18da85199367 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:47:22 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:56:32 2014 +0100
@@ -39,8 +39,7 @@
     end
     handle Pattern.MATCH => no_tac
 
-    val rules = @{thm is_equality_eq} ::
-      ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+    val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
   in
     EVERY' [CSUBGOAL intro_reflp_tac, 
             REPEAT_ALL_NEW (resolve_tac rules)]