src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

   val substitute_noted_thm: (string * thm list) list -> morphism
 
   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
 
   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->

   val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
 end;
 
 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
 struct
-
-fun match_entire_string pat s =
-  let
-    fun match [] [] = true
-      | match [] _ = false
-      | match (ps as #"*" :: ps') cs =
-        match ps' cs orelse (not (null cs) andalso match ps (tl cs))
-      | match _ [] = false
-      | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
-  in
-    match (String.explode pat) (String.explode s)
-  end;
 
 fun map_prod f g (x, y) = (f x, g y);
 
 fun seq_conds f n k xs =
   if k = n then

 val standard_binding = @{binding _};
 
 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 || Parse.string))
-  >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
-
 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*)
 fun WRAP gen_before gen_after xs core_tac =
   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;