1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:55 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:55 2010 +0200
     1.3 @@ -159,13 +159,25 @@
     1.4    Scan.repeat (Scan.one
     1.5      (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
     1.6  
     1.7 +val scan_ident =
     1.8 +  Scan.repeat (Scan.one
     1.9 +    (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
    1.10 +
    1.11  fun dest_Char (Symbol.Char s) = s
    1.12  
    1.13  val string_of = concat o map (dest_Char o Symbol.decode)
    1.14  
    1.15 +val is_atom_ident = forall Symbol.is_ascii_lower
    1.16 +
    1.17 +val is_var_ident =
    1.18 +  forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
    1.19 +
    1.20  val scan_term =
    1.21 -  scan_atom >> (Cons o string_of) || scan_var >> (Var o rpair dummyT o string_of)
    1.22 -
    1.23 +  scan_ident >> (fn s => 
    1.24 +    if is_var_ident s then (Var (string_of s, dummyT))
    1.25 +    else if is_atom_ident s then Cons (string_of s)
    1.26 +    else raise Fail "unexpected")
    1.27 +    
    1.28  val parse_term = fst o Scan.finite Symbol.stopper
    1.29              (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed"))
    1.30                              scan_term)