# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID 74ea14d13247b66cb7d95f238ecb4bcdb23592d7
# Parent  e2abd1ca8d01274b922c3aadd14d811dc56b6672
removing duplicate code

diff -r e2abd1ca8d01 -r 74ea14d13247 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
@@ -60,8 +60,6 @@
   end
   | mk_sumcases _ f T = f T
 
-fun mk_undefined T = Const(@{const_name undefined}, T)
-
 (** abstract syntax **)
 
 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});