--- 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)))
--- 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