# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID edab304696ec3790ae7fec3369d9627e9c6ab9b1
# Parent  89b23fad5e02e981bae11fd05efad7487059a151
adapted parser for options in the predicate compiler

diff -r 89b23fad5e02 -r edab304696ec src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -145,19 +145,17 @@
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
 
-val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)
-
 local structure P = OuterParse
 in
 
 val opt_modes =
-  Scan.optional (P.$$$ "(" |-- P.$$$ "mode" |-- P.$$$ ":" |--
+  Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
    P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
   --| P.$$$ ")" >> SOME) NONE
 
 val scan_params =
   let
-    val scan_bool_param = foldl1 (op ||) (map P.$$$ bool_options)
+    val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
   in
     Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
   end
diff -r 89b23fad5e02 -r edab304696ec src/HOL/ex/RPred.thy
--- a/src/HOL/ex/RPred.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/RPred.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -45,7 +45,7 @@
   where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
-where "map f P = bind P (return o f)"
+  where "map f P = bind P (return o f)"
 
 hide (open) const return bind supp map