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