changeset 43176 | 29a3a1a7794d |
parent 43168 | 467d5b34e1f5 |
child 43182 | 649bada59658 |
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 @@ -584,7 +584,7 @@ fun prop_from_atp ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt in raw_prop_from_atp ctxt textual sym_tab - #> uncombine_term thy #> infer_formula_types ctxt + #> textual ? uncombine_term thy #> infer_formula_types ctxt end (**** Translation of TSTP files to Isar proofs ****)