# HG changeset patch
# User krauss
# Date 1228678883 -3600
# Node ID c8d3a96b69d90679d9c3b1f6790abc74b7e74238
# Parent  3ad09b8d2534ae0927126d54349fb0930bf1508f
killed dead code

diff -r 3ad09b8d2534 -r c8d3a96b69d9 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Dec 06 12:18:05 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Sun Dec 07 20:41:23 2008 +0100
@@ -111,8 +111,6 @@
     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
     val RepC = Const (full Rep_name, newT --> oldT);
     val AbsC = Const (full Abs_name, oldT --> newT);
-    val x_new = Free ("x", newT);
-    val y_old = Free ("y", oldT);
 
     val set' = if def then setC else set;