src/HOL/Import/proof_kernel.ML

 	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
       | _ => Goals.print_exn e
 
 (* 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
 	val {sign,t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)