src/HOL/Tools/res_atp.ML
changeset 15774 9df37a0e935d
parent 15736 1bb0399a9517
child 15779 aed221aff642
--- 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"))