src/HOL/Tools/res_atp.ML
changeset 15774 9df37a0e935d
parent 15736 1bb0399a9517
child 15779 aed221aff642
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4          val prems'' = make_clauses prems'
     1.5          val prems''' = ResAxioms.rm_Eps [] prems''
     1.6          val clss = map ResClause.make_conjecture_clause prems'''
     1.7 -	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss) 
     1.8 +	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
     1.9  	val tfree_lits = ResLib.flat_noDup tfree_litss
    1.10  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    1.11          val hypsfile = File.sysify_path hyps_file
    1.12 @@ -123,7 +123,7 @@
    1.13      let val _ = (warning ("in tptp_inputs_tfrees 0"))
    1.14          val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.15           val _ = (warning ("in tptp_inputs_tfrees 1"))
    1.16 -	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
    1.17 +	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.18          val _ = (warning ("in tptp_inputs_tfrees 2"))
    1.19  	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    1.20           val _ = (warning ("in tptp_inputs_tfrees 3"))