diff -r 276ebec72082 -r 29a15da9c63d src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:43 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:45 2010 +0200
@@ -235,6 +235,8 @@
 val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
   P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
 
+val stats = Scan.optional (Args.$$$ "stats" >> K true) false
+
 val value_options =
   let
     val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
@@ -245,7 +247,8 @@
             compilation_names))
         (Pred, [])
   in
-    Scan.optional (P.$$$ "[" |-- expected_values -- scan_compilation --| P.$$$ "]") (NONE, (Pred, []))
+    Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+      ((NONE, false), (Pred, []))
   end
 
 (* code_pred command and values command *)