# HG changeset patch
# User wenzelm
# Date 1406217509 -7200
# Node ID 4b247a7586c92324bf4746a3ad760822129f2135
# Parent  5bc43a73d768d00b67b3ff0487d75ba734abbd14# Parent  e7fe592ee089357e596cd6249acdb077b985e21a
merged

diff -r e7fe592ee089 -r 4b247a7586c9 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 17:13:26 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jul 24 17:58:29 2014 +0200
@@ -39,6 +39,20 @@
       handle ERROR _ => NONE
   end
 
+fun try_prove_refl_rel ctxt rel =
+  let
+    fun mk_ge_eq x =
+      let
+        val T = fastype_of x
+      in
+        Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $ 
+          (Const (@{const_name HOL.eq}, T)) $ x
+      end;
+    val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
+  in
+     mono_eq_prover ctxt goal
+  end;
+
 fun try_prove_reflexivity ctxt prop =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -178,6 +192,9 @@
     get_body_type_by_rel S (U, V)
   | get_body_type_by_rel _ (U, V)  = (U, V)
 
+fun get_binder_rels (Const (@{const_name "rel_fun"}, _) $ R $ S) = R :: get_binder_rels S
+  | get_binder_rels _ = []
+
 fun force_rty_type ctxt rty rhs = 
   let
     val thy = Proof_Context.theory_of ctxt
@@ -319,11 +336,11 @@
         |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
       end
     
-    val prems = prems_of abs_eq_with_assms
-    val indexed_prems = map_index (apfst (fn x => x + 1)) prems
-    val indexed_assms = map (apsnd (try_prove_reflexivity ctxt)) indexed_prems
-    val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
-    val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
+    val prem_rels = get_binder_rels (quot_thm_rel quot_thm);
+    val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt) 
+      |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the) 
+      |> map (apsnd (fn assm => assm RS @{thm ge_eq_refl}))
+    val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms
   in
     simplify_code_eq ctxt abs_eq
   end