--- 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
--- 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 _ = "";
--- 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