author | bulwahn |
Fri, 08 Apr 2011 16:31:14 +0200 | |
changeset 43169 | 74ea14d13247 |
parent 43168 | e2abd1ca8d01 |
child 43170 | c664cc5cc5e9 |
1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200 1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200 1.3 @@ -60,8 +60,6 @@ 1.4 end 1.5 | mk_sumcases _ f T = f T 1.6 1.7 -fun mk_undefined T = Const(@{const_name undefined}, T) 1.8 - 1.9 (** abstract syntax **) 1.10 1.11 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});