--- 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)))