# HG changeset patch
# User wenzelm
# Date 1082984085 -7200
# Node ID 3d760a971fde80cdd81f736acedcf1072cc08d6b
# Parent  79bac83b2c2754d5f309d72edcfe39e66847cd17
use Syntax.is_identifier;

diff -r 79bac83b2c27 -r 3d760a971fde src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Apr 26 14:53:29 2004 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon Apr 26 14:54:45 2004 +0200
@@ -170,10 +170,13 @@
 
 (* Compatibility. *)
 
-fun mk_syn c = if Symbol.is_identifier c then NoSyn else Syntax.literal c
+(* FIXME lookup inner syntax!? *)
+fun mk_syn c = if Syntax.is_identifier c then NoSyn else Syntax.literal c
 
+(* FIXME lookup outer syntax!? *)
 val keywords = ["open"]
-fun quotename c = if Symbol.is_identifier c andalso not (c mem keywords) then c else quote c
+fun quotename c =
+  if Syntax.is_identifier c andalso not (c mem_string keywords) then c else quote c
 
 fun smart_string_of_cterm ct =
     let
diff -r 79bac83b2c27 -r 3d760a971fde src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:53:29 2004 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:54:45 2004 +0200
@@ -227,7 +227,7 @@
 fun name_of_typ (Type (s, Ts)) =
       let val s' = Sign.base_name s
       in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
-        [if Symbol.is_identifier s' then s' else "x"])
+        [if Syntax.is_identifier s' then s' else "x"])
       end
   | name_of_typ _ = "";
 
diff -r 79bac83b2c27 -r 3d760a971fde src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Apr 26 14:53:29 2004 +0200
+++ b/src/Pure/tactic.ML	Mon Apr 26 14:54:45 2004 +0200
@@ -566,7 +566,7 @@
 (*Calling this will generate the warning "Same as previous level" since
   it affects nothing but the names of bound variables!*)
 fun rename_params_tac xs i =
-  case Library.find_first (not o Symbol.is_identifier) xs of
+  case Library.find_first (not o Syntax.is_identifier) xs of
       Some x => error ("Not an identifier: " ^ x)
     | None => 
        (if !Logic.auto_rename