# HG changeset patch
# User bulwahn
# Date 1280417275 -7200
# Node ID 2a9c14d9d2ef3380e496d44563a794130cbed97e
# Parent  3d5e2b7d13747e9aaf4342677a1ed224b61fa2cb
correcting scanning

diff -r 3d5e2b7d1374 -r 2a9c14d9d2ef src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:55 2010 +0200
@@ -159,13 +159,25 @@
   Scan.repeat (Scan.one
     (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
 
+val scan_ident =
+  Scan.repeat (Scan.one
+    (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
+
 fun dest_Char (Symbol.Char s) = s
 
 val string_of = concat o map (dest_Char o Symbol.decode)
 
+val is_atom_ident = forall Symbol.is_ascii_lower
+
+val is_var_ident =
+  forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+
 val scan_term =
-  scan_atom >> (Cons o string_of) || scan_var >> (Var o rpair dummyT o string_of)
-
+  scan_ident >> (fn s => 
+    if is_var_ident s then (Var (string_of s, dummyT))
+    else if is_atom_ident s then Cons (string_of s)
+    else raise Fail "unexpected")
+    
 val parse_term = fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed"))
                             scan_term)