# 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