diff -r 20aa19ecf2cc -r 9e0ecb66d6a7 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -1028,7 +1028,7 @@
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "values_prolog"}
+  Outer_Syntax.command @{command_spec "values_prolog"}
     "enumerate and print comprehensions"
     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
      >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))