# HG changeset patch
# User kuncar
# Date 1393336974 -3600
# Node ID e6edd47f14831af58d0f801c18d791f8563a0155
# Parent  07906fc6af7a1e8db706769a2e1b98d71abbe731
the rules are not needed due to 1726f46d2aa8

diff -r 07906fc6af7a -r e6edd47f1483 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 15:02:20 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 15:02:54 2014 +0100
@@ -29,7 +29,7 @@
 
 fun mono_eq_prover ctxt prop =
   let
-    val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+    val rules = Lifting_Info.get_reflexivity_rules ctxt
   in
     SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
       handle ERROR _ => NONE