use Syntax.is_identifier;
authorwenzelm
Mon Apr 26 14:54:45 2004 +0200 (2004-04-26)
changeset 146733d760a971fde
parent 14672 79bac83b2c27
child 14674 3506a9af46fc
use Syntax.is_identifier;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/datatype_aux.ML
src/Pure/tactic.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Apr 26 14:53:29 2004 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Apr 26 14:54:45 2004 +0200
     1.3 @@ -170,10 +170,13 @@
     1.4  
     1.5  (* Compatibility. *)
     1.6  
     1.7 -fun mk_syn c = if Symbol.is_identifier c then NoSyn else Syntax.literal c
     1.8 +(* FIXME lookup inner syntax!? *)
     1.9 +fun mk_syn c = if Syntax.is_identifier c then NoSyn else Syntax.literal c
    1.10  
    1.11 +(* FIXME lookup outer syntax!? *)
    1.12  val keywords = ["open"]
    1.13 -fun quotename c = if Symbol.is_identifier c andalso not (c mem keywords) then c else quote c
    1.14 +fun quotename c =
    1.15 +  if Syntax.is_identifier c andalso not (c mem_string keywords) then c else quote c
    1.16  
    1.17  fun smart_string_of_cterm ct =
    1.18      let
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:53:29 2004 +0200
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:54:45 2004 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4  fun name_of_typ (Type (s, Ts)) =
     2.5        let val s' = Sign.base_name s
     2.6        in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
     2.7 -        [if Symbol.is_identifier s' then s' else "x"])
     2.8 +        [if Syntax.is_identifier s' then s' else "x"])
     2.9        end
    2.10    | name_of_typ _ = "";
    2.11  
     3.1 --- a/src/Pure/tactic.ML	Mon Apr 26 14:53:29 2004 +0200
     3.2 +++ b/src/Pure/tactic.ML	Mon Apr 26 14:54:45 2004 +0200
     3.3 @@ -566,7 +566,7 @@
     3.4  (*Calling this will generate the warning "Same as previous level" since
     3.5    it affects nothing but the names of bound variables!*)
     3.6  fun rename_params_tac xs i =
     3.7 -  case Library.find_first (not o Symbol.is_identifier) xs of
     3.8 +  case Library.find_first (not o Syntax.is_identifier) xs of
     3.9        Some x => error ("Not an identifier: " ^ x)
    3.10      | None => 
    3.11         (if !Logic.auto_rename