--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100
@@ -161,7 +161,8 @@
| add_fact _ _ = I
fun used_facts_in_tstplike_proof fact_names =
- atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
+ atp_proof_from_tstplike_string false
+ #> rpair [] #-> fold (add_fact fact_names)
val split_used_facts =
List.partition (curry (op =) Chained o snd)
@@ -608,7 +609,7 @@
let
val lines =
tstplike_proof
- |> atp_proof_from_tstplike_string
+ |> atp_proof_from_tstplike_string true
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
|> decode_lines ctxt type_sys tfrees