# HG changeset patch
# User bulwahn
# Date 1320834893 -3600
# Node ID cf31fe74b05a6953d98fd8885467b4b38a00cd35
# Parent  bf39b07a7a8eec96bbddd83c0209d053e59b48ef
tuned

diff -r bf39b07a7a8e -r cf31fe74b05a src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- 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