--- a/src/HOL/Tools/res_atp.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Apr 19 18:08:44 2005 +0200
@@ -104,7 +104,7 @@
val prems'' = make_clauses prems'
val prems''' = ResAxioms.rm_Eps [] prems''
val clss = map ResClause.make_conjecture_clause prems'''
- val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
+ val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val tfree_lits = ResLib.flat_noDup tfree_litss
val tfree_clss = map ResClause.tfree_clause tfree_lits
val hypsfile = File.sysify_path hyps_file
@@ -123,7 +123,7 @@
let val _ = (warning ("in tptp_inputs_tfrees 0"))
val clss = map (ResClause.make_conjecture_clause_thm) thms
val _ = (warning ("in tptp_inputs_tfrees 1"))
- val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
+ val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val _ = (warning ("in tptp_inputs_tfrees 2"))
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
val _ = (warning ("in tptp_inputs_tfrees 3"))