--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon May 21 16:36:48 2012 +0200
@@ -14,11 +14,6 @@
val abs_fun: Proof.context -> typ * typ -> term
val equiv_relation: Proof.context -> typ * typ -> term
-
- val quot_thm_rel: thm -> term
- val quot_thm_abs: thm -> term
- val quot_thm_rep: thm -> term
- val quot_thm_rty_qty: thm -> typ * typ
end
structure Lifting_Term: LIFTING_TERM =
@@ -79,31 +74,6 @@
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
-(*
- quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
- for destructing quotient theorems (Quotient R Abs Rep 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 =
- case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
- (_, abs, _, _) => abs
-
-fun quot_thm_rep quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
- (_, _, rep, _) => rep
-
-fun quot_thm_rty_qty quot_thm =
- let
- val abs = quot_thm_abs quot_thm
- val abs_type = fastype_of abs
- in
- (domain_type abs_type, range_type abs_type)
- end
-
fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
if provided_rty_name <> rty_of_qty_name then
raise QUOT_THM_INTERNAL (Pretty.block