# HG changeset patch
# User blanchet
# Date 1310649277 -7200
# Node ID d439173f3daf81f0eb5bf3a43d9d2e78dc921592
# Parent  89082fd9e32de78b5ecc35a7ac2e0eab25ebcaa8
unbreak Nitrox's parsing

diff -r 89082fd9e32d -r d439173f3daf src/HOL/Tools/Nitpick/nitrox.ML
--- a/src/HOL/Tools/Nitpick/nitrox.ML	Thu Jul 14 00:21:56 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Thu Jul 14 15:14:37 2011 +0200
@@ -21,7 +21,8 @@
 
 exception SYNTAX of string
 
-val parse_keyword = Scan.this_string
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val tptp_explode = raw_explode o strip_spaces true is_ident_char
 
 fun parse_file_path (c :: ss) =
     if c = "'" orelse c = "\"" then
@@ -33,24 +34,20 @@
 fun parse_include x =
   let
     val (file_name, rest) =
-      (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
+      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
        --| $$ ".") x
     val path = file_name |> Path.explode
     val path =
       path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
-  in
-    ((), (path |> File.read
-               |> strip_spaces true (K true)
-               |> raw_explode) @ rest)
-  end
+  in ((), (path |> File.read |> tptp_explode) @ rest) end
 
 val parse_fof_or_cnf =
-  (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
+  (Scan.this_string "fof" || Scan.this_string "cnf") |-- $$ "(" |--
   Scan.many (not_equal ",") |-- $$ "," |--
-  (parse_keyword "axiom" || parse_keyword "definition"
-   || parse_keyword "theorem" || parse_keyword "lemma"
-   || parse_keyword "hypothesis" || parse_keyword "conjecture"
-   || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
+  (Scan.this_string "axiom" || Scan.this_string "definition"
+   || Scan.this_string "theorem" || Scan.this_string "lemma"
+   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
+   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
       --| $$ ")" --| $$ "."
   >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
 
@@ -62,7 +59,7 @@
   Scan.finite Symbol.stopper
       (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
                   parse_problem))
-  o raw_explode o strip_spaces true (K true)
+  o tptp_explode
 
 val boolT = @{typ bool}
 val iotaT = @{typ iota}