# HG changeset patch
# User wenzelm
# Date 1128720540 -7200
# Node ID ccba4e9000239f2da80535168871575559c083a2
# Parent  86c46583670f489420db9cc7a9a2a65619575a82
removed obsolete comment;

diff -r 86c46583670f -r ccba4e900023 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Fri Oct 07 22:59:26 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Fri Oct 07 23:29:00 2005 +0200
@@ -119,8 +119,6 @@
             | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
   in match (space_explode "*" pat) str end;
 
-(*filter that just looks for a string in the name,
-  substring match only (no regexps are performed)*)
 fun filter_name str_pat (thmref, _) =
   if match_string str_pat (PureThy.name_of_thmref thmref)
   then SOME (0, 0) else NONE;