src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15774 9df37a0e935d
parent 15736 1bb0399a9517
child 15782 a1863ea9052b
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4                                                val numbers = 0 upto (num_of_cls -1)
     1.5                                                val multi_name = multi name num_of_cls []
     1.6                                            in 
     1.7 -                                              zip multi_name numbers
     1.8 +                                              ListPair.zip (multi_name,numbers)
     1.9                                            end;
    1.10  
    1.11  fun stick []  = []
    1.12 @@ -108,7 +108,7 @@
    1.13                                      (* get (name, thm) pairs for claset rules *)
    1.14                                     (*******************************************)
    1.15  
    1.16 -                                   val names_rules = zip good_names name_fol_cs;
    1.17 +                                   val names_rules = ListPair.zip (good_names,name_fol_cs);
    1.18                                     
    1.19                                     val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
    1.20  
    1.21 @@ -118,7 +118,7 @@
    1.22                                     val stick_clasrls =  map stick claset_tptp_strs;
    1.23                                     (* stick stick_clasrls length is 172*)
    1.24  
    1.25 -                                   val name_stick = zip good_names stick_clasrls;
    1.26 +                                   val name_stick = ListPair.zip (good_names,stick_clasrls);
    1.27  
    1.28                                     val cl_name_nums =map clause_numbering name_stick;
    1.29                                         
    1.30 @@ -169,7 +169,7 @@
    1.31                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    1.32  
    1.33                                      val stick_strs = map stick simpset_tptp_strs;
    1.34 -                                    val name_stick = zip simp_names stick_strs;
    1.35 +                                    val name_stick = ListPair.zip (simp_names,stick_strs);
    1.36  
    1.37                                      val name_nums =map clause_numbering name_stick;
    1.38                                      (* length 2409*)