author | bulwahn |
Fri, 08 Apr 2011 16:31:14 +0200 | |
changeset 42309 | 74ea14d13247 |
parent 42308 | e2abd1ca8d01 |
child 42310 | c664cc5cc5e9 |
--- 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"});