--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 11:22:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 11:38:23 2010 +0200
@@ -109,7 +109,7 @@
(* needed for SPASS's output format *)
fun repair_name _ "$true" = "c_True"
| repair_name _ "$false" = "c_False"
- | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
+ | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
| repair_name _ "equal" = "c_equal" (* probably not needed *)
| repair_name pool s = ugly_name pool s
(* Generalized first-order terms, which include file names, numbers, etc. *)
@@ -199,7 +199,6 @@
(* Syntax: <num>[0:<inference><annotations>]
<cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
-|> tap (fn _ => priority ("*** processing " ^ PolyML.makestring num)) (* ### *)
fun parse_spass_line pool =
parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
@@ -491,7 +490,7 @@
fun add_line _ _ (line as Definition _) lines = line :: lines
| add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
(* No dependencies: axiom, conjecture clause, or internal axioms
- (Vampire). *)
+ (Vampire 11). *)
if is_axiom_clause_number thm_names num then
(* Axioms are not proof lines. *)
if is_only_type_information t then
@@ -538,7 +537,8 @@
if is_only_type_information t orelse
not (null (Term.add_tvars t [])) orelse
exists_subterm is_bad_free t orelse
- (length deps < 2 orelse j mod shrink_factor <> 0) then
+ (not (null lines) andalso (* last line must be kept *)
+ (length deps < 2 orelse j mod shrink_factor <> 0)) then
map (replace_deps_in_line (num, deps)) lines (* delete line *)
else
Inference (num, t, deps) :: lines)