# HG changeset patch
# User wenzelm
# Date 1175638274 -7200
# Node ID 4b1ecb19b411e542d65af9ce71e9091b218c5dd3
# Parent  f315da9400fbe9afd94d7bc3325a0f5fd54a3e3c
added scanwords from library.ML (for obsolete rename_tac);

diff -r f315da9400fb -r 4b1ecb19b411 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Apr 04 00:11:13 2007 +0200
+++ b/src/Pure/tactic.ML	Wed Apr 04 00:11:14 2007 +0200
@@ -515,6 +515,15 @@
              Logic.auto_rename := false)
         else (); PRIMITIVE (rename_params_rule (xs, i)));
 
+(*scan a list of characters into "words" composed of "letters" (recognized by
+  is_let) and separated by any number of non-"letters"*)
+fun scanwords is_let cs =
+  let fun scan1 [] = []
+        | scan1 cs =
+            let val (lets, rest) = take_prefix is_let cs
+            in implode lets :: scanwords is_let rest end;
+  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
+
 fun rename_tac str i =
   let val cs = Symbol.explode str in
   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of