src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 41742 11e862c68b40
parent 41203 1393514094d7
child 42180 a6c141925a8a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4    val split_used_facts :
     1.5      (string * locality) list
     1.6      -> (string * locality) list * (string * locality) list
     1.7 +  val metis_proof_text : metis_params -> text_result
     1.8    val isar_proof_text : isar_params -> metis_params -> text_result
     1.9    val proof_text : bool -> isar_params -> metis_params -> text_result
    1.10  end;
    1.11 @@ -165,9 +166,13 @@
    1.12      append (resolve_fact fact_names name)
    1.13    | add_fact _ _ = I
    1.14  
    1.15 -fun used_facts_in_tstplike_proof fact_names =
    1.16 -  atp_proof_from_tstplike_string false
    1.17 -  #> rpair [] #-> fold (add_fact fact_names)
    1.18 +fun used_facts_in_tstplike_proof fact_names tstplike_proof =
    1.19 +  if tstplike_proof = "" then
    1.20 +    Vector.foldl (op @) [] fact_names
    1.21 +  else
    1.22 +    tstplike_proof
    1.23 +    |> atp_proof_from_tstplike_string false
    1.24 +    |> rpair [] |-> fold (add_fact fact_names)
    1.25  
    1.26  val split_used_facts =
    1.27    List.partition (curry (op =) Chained o snd)