diff -r 1272cfc7b910 -r b70fe083694d src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -155,6 +155,8 @@
 local structure P = OuterParse
 in
 
+(* Parser for mode annotations *)
+
 (*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
 datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
 
@@ -185,16 +187,37 @@
   Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
     P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
 
-val scan_params =
+(* Parser for options *)
+
+val scan_options =
   let
-    val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
+    val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
   in
-    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
+    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") []
   end
 
+val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val value_options =
+  let
+    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+    val random = Scan.optional (Args.$$$ "random" >> K true) false
+    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
+  in
+    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
+      (NONE, (false, false))
+  end
+
+(* code_pred command and values command *)
+
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd)
+  OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+  (opt_print_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
+        (Predicate_Compile_Core.values_cmd modes options k t)));
 
 end