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;