--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 12:10:19 2014 +0100
@@ -61,8 +61,10 @@
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
-val quickcheck_generator_cmd = gen_quickcheck_generator
- (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+val quickcheck_generator_cmd =
+ gen_quickcheck_generator
+ (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false})
+ Syntax.read_term
val _ =
Outer_Syntax.command @{command_spec "quickcheck_generator"}