# HG changeset patch
# User kuncar
# Date 1353936036 -3600
# Node ID 536ab2e82eade785ad86b13b01bae6c8ebeadf2f
# Parent  f478f4ca7f193aeae955d05e88ff9a9aa6a80ab0
quot_thm_crel

diff -r f478f4ca7f19 -r 536ab2e82ead src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Nov 26 14:15:48 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Nov 26 14:20:36 2012 +0100
@@ -14,6 +14,7 @@
   val quot_thm_rel: thm -> term
   val quot_thm_abs: thm -> term
   val quot_thm_rep: thm -> term
+  val quot_thm_crel: thm -> term
   val quot_thm_rty_qty: thm -> typ * typ
 end;
 
@@ -54,6 +55,10 @@
   case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
     (_, _, rep, _) => rep
 
+fun quot_thm_crel quot_thm =
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (_, _, _, crel) => crel
+
 fun quot_thm_rty_qty quot_thm =
   let
     val abs = quot_thm_abs quot_thm