diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 18:45:48 2014 +0200
@@ -71,7 +71,6 @@
   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
 
@@ -87,18 +86,6 @@
 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 =
@@ -262,12 +249,6 @@
 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*)