1.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Feb 12 12:35:45 2009 -0800
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Fri Feb 13 07:53:38 2009 +1100
     1.3 @@ -103,21 +103,10 @@
     1.4  
     1.5  (* filter_name *)
     1.6  
     1.7 -fun match_string pat str =
     1.8 -  let
     1.9 -    fun match [] _ = true
    1.10 -      | match (p :: ps) s =
    1.11 -          size p <= size s andalso
    1.12 -            (case try (unprefix p) s of
    1.13 -              SOME s' => match ps s'
    1.14 -            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
    1.15 -  in match (space_explode "*" pat) str end;
    1.16 -
    1.17  fun filter_name str_pat (thmref, _) =
    1.18    if match_string str_pat (Facts.name_of_ref thmref)
    1.19    then SOME (0, 0) else NONE;
    1.20  
    1.21 -
    1.22  (* filter intro/elim/dest/solves rules *)
    1.23  
    1.24  fun filter_dest ctxt goal (_, thm) =