added scanwords from library.ML (for obsolete rename_tac);
authorwenzelm
Wed Apr 04 00:11:14 2007 +0200 (2007-04-04)
changeset 225834b1ecb19b411
parent 22582 f315da9400fb
child 22584 d0f0f37ec346
added scanwords from library.ML (for obsolete rename_tac);
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Apr 04 00:11:13 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Apr 04 00:11:14 2007 +0200
     1.3 @@ -515,6 +515,15 @@
     1.4               Logic.auto_rename := false)
     1.5          else (); PRIMITIVE (rename_params_rule (xs, i)));
     1.6  
     1.7 +(*scan a list of characters into "words" composed of "letters" (recognized by
     1.8 +  is_let) and separated by any number of non-"letters"*)
     1.9 +fun scanwords is_let cs =
    1.10 +  let fun scan1 [] = []
    1.11 +        | scan1 cs =
    1.12 +            let val (lets, rest) = take_prefix is_let cs
    1.13 +            in implode lets :: scanwords is_let rest end;
    1.14 +  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
    1.15 +
    1.16  fun rename_tac str i =
    1.17    let val cs = Symbol.explode str in
    1.18    case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of