src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -76,6 +76,7 @@
   val standard_binding: binding
   val parse_binding_colon: binding parser
   val parse_opt_binding_colon: binding parser
+  val parse_plugins: (string -> bool) parser
 
   val ss_only: thm list -> Proof.context -> Proof.context
 
@@ -268,6 +269,11 @@
 val parse_binding_colon = Parse.binding --| @{keyword ":"};
 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
 
+val parse_plugins =
+  Parse.reserved "plugins" |--
+    ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
+     -- Scan.repeat Parse.short_ident) >> (fn (modif, ss) => modif o member (op =) ss);
+
 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
 
 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)