author | krauss |
Sun, 07 Dec 2008 20:41:23 +0100 | |
changeset 29052 | c8d3a96b69d9 |
parent 29009 | 3ad09b8d2534 |
child 29053 | 077fb9b16119 |
--- 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;