# HG changeset patch
# User huffman
# Date 1333701466 -7200
# Node ID 9f38eff9c45f3b19db7a60e4558480105d9f5560
# Parent  c608111857d19e22c45b4a1670b02c5154afc11e
add function dest_Quotient

diff -r c608111857d1 -r 9f38eff9c45f src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Apr 06 09:35:47 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Fri Apr 06 10:37:46 2012 +0200
@@ -85,29 +85,21 @@
 
 exception NOT_IMPL of string
 
-fun quot_thm_rel quot_thm = 
-  let
-    val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) = 
-      (HOLogic.dest_Trueprop o prop_of) quot_thm
-  in
-    rel
-  end
+fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
+      = (rel, abs, rep, cr)
+  | dest_Quotient t = raise TERM ("dest_Quotient", [t])
+
+fun quot_thm_rel quot_thm =
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (rel, _, _, _) => rel
 
 fun quot_thm_abs quot_thm =
-  let
-    val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) = 
-      (HOLogic.dest_Trueprop o prop_of) quot_thm
-  in
-    abs
-  end
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (_, abs, _, _) => abs
 
 fun quot_thm_rep quot_thm =
-  let
-    val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) = 
-      (HOLogic.dest_Trueprop o prop_of) quot_thm
-  in
-    rep
-  end
+  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
+    (_, _, rep, _) => rep
 
 fun quot_thm_rty_qty quot_thm =
   let