adapted to baroque chars;
authorwenzelm
Mon Mar 09 16:09:06 1998 +0100 (1998-03-09)
changeset 46932e47ea2c6109
parent 4692 748f4e365d14
child 4694 92e12a04dca7
adapted to baroque chars;
src/Pure/logic.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/logic.ML	Mon Mar 09 16:08:37 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Mon Mar 09 16:09:06 1998 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  
     1.5  (*rename_prefix is not exported; it is set by this function.*)
     1.6  fun set_rename_prefix a =
     1.7 -    if a<>"" andalso forall is_letter (explode a)
     1.8 +    if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
     1.9      then  (rename_prefix := a;  auto_rename := true)
    1.10      else  error"rename prefix must be nonempty and consist of letters";
    1.11  
     2.1 --- a/src/Pure/tactic.ML	Mon Mar 09 16:08:37 1998 +0100
     2.2 +++ b/src/Pure/tactic.ML	Mon Mar 09 16:09:06 1998 +0100
     2.3 @@ -528,14 +528,14 @@
     2.4  (*Calling this will generate the warning "Same as previous level" since
     2.5    it affects nothing but the names of bound variables!*)
     2.6  fun rename_tac str i = 
     2.7 -  let val cs = explode str 
     2.8 +  let val cs = Symbol.explode str 
     2.9    in  
    2.10    if !Logic.auto_rename 
    2.11    then (warning "Resetting Logic.auto_rename"; 
    2.12  	Logic.auto_rename := false)
    2.13    else ();
    2.14 -  case #2 (take_prefix (is_letdig orf is_blank) cs) of
    2.15 -      [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
    2.16 +  case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
    2.17 +      [] => PRIMITIVE (rename_params_rule (scanwords Symbol.is_letdig cs, i))
    2.18      | c::_ => error ("Illegal character: " ^ c)
    2.19    end;
    2.20