# HG changeset patch
# User wenzelm
# Date 1354289677 -3600
# Node ID dab1a3d3ba30cd79db615eed37a3c087985bd542
# Parent  dceb1daa185c900d39632908654e4d883b9a8ac5# Parent  3d6a4135a54f5bbfc8ea9a771ad05cd62efb8206
merged

diff -r dceb1daa185c -r dab1a3d3ba30 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Nov 30 16:34:11 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML	Fri Nov 30 16:34:37 2012 +0100
@@ -251,11 +251,11 @@
 val scan_ident =
   Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
 
-fun is_ident [] = false
-  | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss;
-
 fun is_identifier s =
-  Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none));
+  Symbol.is_ascii_identifier s orelse
+    (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
+      SOME (_, []) => true
+    | _ => false);
 
 end;