# HG changeset patch
# User blanchet
# Date 1375107215 -7200
# Node ID 1ac8a0d0ddb1190782daa361a87349eb9e9f9f58
# Parent  4183c32197455adbbb8f29ae11b1d86b08c2cddc
parse nonnumeric identifiers in E proofs correctly

diff -r 4183c3219745 -r 1ac8a0d0ddb1 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 29 15:42:04 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 29 16:13:35 2013 +0200
@@ -260,7 +260,7 @@
   (parse_file_source >> File_Source
    || parse_inference_source >> Inference_Source
    || skip_introduced >> K dummy_inference (* for Vampire *)
-   || scan_nat >> (fn s => Inference_Source ("", [s])) (* for E *)
+   || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *)
    || skip_term >> K dummy_inference) x
 
 fun list_app (f, args) =
@@ -506,7 +506,7 @@
     case core_of_agsyhol_proof tstp of
       SOME facts => facts |> map (core_inference agsyhol_coreN)
     | NONE =>
-      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
+      tstp ^ "$"  (* the $ sign acts as a sentinel (FIXME: needed?) *)
       |> parse_proof problem
       |> perhaps (try (sort (vampire_step_name_ord o pairself #1)))
 
diff -r 4183c3219745 -r 1ac8a0d0ddb1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Jul 29 15:42:04 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Jul 29 16:13:35 2013 +0200
@@ -327,8 +327,7 @@
 
 val add_labels_of_proof =
   steps_of_proof #> fold_isar_steps
-    (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls
-                         | _ => I))
+    (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I))
 
 fun kill_useless_labels_in_proof proof =
   let