# HG changeset patch
# User huffman
# Date 1267826136 28800
# Node ID 47d68e33ca29d5b5d6cf660924efed42b732f1d3
# Parent  f638444c966793b318be5151b967dfe1ca4c8ed2
remove dead code

diff -r f638444c9667 -r 47d68e33ca29 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Mar 05 13:33:17 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Mar 05 13:55:36 2010 -0800
@@ -99,26 +99,13 @@
 infix -->>;
 infix 9 `;
 
-val deflT = @{typ "udom alg_defl"};
-
 fun mapT (T as Type (_, Ts)) =
     (map (fn T => T ->> T) Ts) -->> (T ->> T)
   | mapT T = T ->> T;
 
-fun mk_Rep_of T =
-  Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
-
-fun coerce_const T = Const (@{const_name coerce}, T);
-
-fun isodefl_const T =
-  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
-
 fun mk_deflation t =
   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
 
-(* splits a cterm into the right and lefthand sides of equality *)
-fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
-
 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
 
 (******************************************************************************)