--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 14:47:38 2011 +1100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 11:34:53 2011 +0100
@@ -174,8 +174,8 @@
fun get_finite_types ctxt =
fst (chop (Config.get ctxt Quickcheck.finite_type_size)
- (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
- "Enum.finite_4", "Enum.finite_5"]))
+ [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"},
+ @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}])
exception WELLSORTED of string