more tidying of libraries in Reconstruction
authorpaulson
Tue Apr 19 18:08:44 2005 +0200 (2005-04-19)
changeset 157749df37a0e935d
parent 15773 f14ae2432710
child 15775 d8dd2fffa692
more tidying of libraries in Reconstruction
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/recon_gandalf_base.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_lib.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -114,10 +114,10 @@
     1.4    blastdata.ML cladata.ML \
     1.5   Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
     1.6   Tools/res_axioms.ML Tools/res_types_sorts.ML \
     1.7 - Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
     1.8 + Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\
     1.9   Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
    1.10   Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
    1.11 - Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
    1.12 + Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML  \
    1.13   Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
    1.14    document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    1.15  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
     2.1 --- a/src/HOL/Reconstruction.thy	Tue Apr 19 15:15:06 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Tue Apr 19 18:08:44 2005 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4  	  "Tools/res_types_sorts.ML"
     2.5  
     2.6            "Tools/ATP/recon_prelim.ML"
     2.7 -	  "Tools/ATP/recon_gandalf_base.ML"
     2.8   	  "Tools/ATP/recon_order_clauses.ML"
     2.9   	  "Tools/ATP/recon_translate_proof.ML"
    2.10   	  "Tools/ATP/recon_parse.ML"
     3.1 --- a/src/HOL/Tools/ATP/recon_gandalf_base.ML	Tue Apr 19 15:15:06 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,39 +0,0 @@
     3.4 -structure Recon_Base =
     3.5 -struct
     3.6 -
     3.7 -(* Auxiliary functions *)
     3.8 -
     3.9 -exception Assertion of string;
    3.10 -
    3.11 -val DEBUG = ref true;
    3.12 -fun TRACE s = if !DEBUG then print s else ();
    3.13 -
    3.14 -exception Noassoc;
    3.15 -fun assoc a [] = raise Noassoc
    3.16 -  | assoc a ((x, y)::t) = if a = x then y else assoc a t;
    3.17 -fun assoc_exists a [] = false
    3.18 -  | assoc_exists a ((x, y)::t) = if a = x then true else assoc_exists a t;
    3.19 -fun assoc_update (a, b) [] = raise Noassoc
    3.20 -  | assoc_update (a, b) ((x, y)::t)
    3.21 -    = if a = x then (a, b)::t else (x, y)::(assoc_update (a, b) t)
    3.22 -fun assoc_inv a [] = raise Noassoc
    3.23 -  | assoc_inv a ((x, y)::t) = if a = y then x else assoc a t;
    3.24 -fun assoc_inv_exists a [] = false
    3.25 -  | assoc_inv_exists a ((x, y)::t) = if a = y then true else assoc_inv_exists a t;
    3.26 -
    3.27 -fun is_mem x [] = false
    3.28 -  | is_mem x (h::t) = (x = h) orelse is_mem x t;
    3.29 -fun elt 0 (h::t) = h
    3.30 -  | elt n (h::t) = elt (n - 1) t
    3.31 -  | elt n l = raise (Assertion "elt: out of range");
    3.32 -fun remove_elt _ [] = raise (Assertion "remove_elt: out of range")
    3.33 -  | remove_elt 0 (h::t) = t
    3.34 -  | remove_elt n (h::t) = h::(remove_elt (n - 1) t);
    3.35 -fun elt_num x [] = raise (Assertion "elt_num: not in list")
    3.36 -  | elt_num x (h::t) = if h = x then 0 else 1 + elt_num x t;
    3.37 -fun set_add x l = if is_mem x l then l else x::l;
    3.38 -
    3.39 -fun iter f a [] = a
    3.40 -  | iter f a (h::t) = f h (iter f a t);
    3.41 -
    3.42 -end;
     4.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 19 15:15:06 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 19 18:08:44 2005 +0200
     4.3 @@ -2,27 +2,16 @@
     4.4  (* Reorder clauses for use in binary resolution *)
     4.5  (*----------------------------------------------*)
     4.6  
     4.7 -fun drop n [] = []
     4.8 -|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
     4.9 -
    4.10  fun remove_nth n [] = []
    4.11  |   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
    4.12  
    4.13 -fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    4.14 +(*Differs from List.nth: it counts from 1 rather than from 0*)
    4.15 +fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs))
    4.16  
    4.17  
    4.18  exception Not_in_list;  
    4.19  
    4.20  
    4.21 -fun zip xs [] = []
    4.22 -|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    4.23 -
    4.24 -
    4.25 -fun unzip [] = ([],[])
    4.26 -    | unzip((x,y)::pairs) =
    4.27 -	  let val (xs,ys) = unzip pairs
    4.28 -	  in  (x::xs, y::ys)  end;
    4.29 -
    4.30  fun numlist 0 = []
    4.31  |   numlist n = (numlist (n - 1))@[n]
    4.32  
    4.33 @@ -39,13 +28,6 @@
    4.34  
    4.35  (* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
    4.36  
    4.37 -fun assoc3 a [] = raise Recon_Base.Noassoc
    4.38 -  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
    4.39 -
    4.40 -
    4.41 -fun third (a,b,c) = c;
    4.42 -
    4.43 -
    4.44   fun takeUntil ch [] res  = (res, [])
    4.45   |   takeUntil ch (x::xs) res = if   x = ch 
    4.46                                  then
    4.47 @@ -70,12 +52,12 @@
    4.48                         then 
    4.49                             let val (left, right) = takeUntil "=" str []
    4.50                             in
    4.51 -                               ((butlast left), (drop 1 right))
    4.52 +                               (butlast left, tl right)
    4.53                             end
    4.54                         else                  (* is an inequality *)
    4.55                             let val (left, right) = takeUntil "~" str []
    4.56                             in 
    4.57 -                              ((butlast left), (drop 2 right))
    4.58 +                              (butlast left, tl (tl right))
    4.59                             end
    4.60                  
    4.61  
    4.62 @@ -101,23 +83,16 @@
    4.63  
    4.64  
    4.65  
    4.66 -fun var_pos_eq vars x y = let val xs = explode x
    4.67 +fun var_pos_eq vars x y = String.size x = String.size y andalso
    4.68 +			  let val xs = explode x
    4.69                                val ys = explode y
    4.70 +                              val xsys = ListPair.zip (xs,ys)
    4.71 +                              val are_var_pairs = map (var_equiv vars) xsys
    4.72                            in
    4.73 -                              if not_equal (length xs) (length ys)
    4.74 -                              then 
    4.75 -                                  false
    4.76 -                              else
    4.77 -                                  let val xsys = zip xs ys
    4.78 -                                      val are_var_pairs = map (var_equiv vars) xsys
    4.79 -                                  in
    4.80 -                                      all_true are_var_pairs 
    4.81 -                                  end
    4.82 +                              all_true are_var_pairs 
    4.83                            end
    4.84  
    4.85  
    4.86 -
    4.87 -
    4.88  fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
    4.89      |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
    4.90                                   let val y = explode x 
     5.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 19 15:15:06 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 19 18:08:44 2005 +0200
     5.3 @@ -116,7 +116,9 @@
     5.4  fun get_step_nums [] nums = nums
     5.5  |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
     5.6  
     5.7 -fun assoc_snd a [] = raise Recon_Base.Noassoc
     5.8 +exception Noassoc;
     5.9 +
    5.10 +fun assoc_snd a [] = raise Noassoc
    5.11    | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
    5.12  
    5.13  (* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
    5.14 @@ -125,13 +127,10 @@
    5.15  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    5.16  *)
    5.17  (*FIX - should this have vars in it? *)
    5.18 -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))                        
    5.19 -                               in 
    5.20 -                                   true
    5.21 -                              end
    5.22 -                              handle EXCEP => false
    5.23 +fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) 
    5.24 +                               handle _ => false
    5.25  
    5.26 -fun assoc_out_of_order a [] = raise Recon_Base.Noassoc
    5.27 +fun assoc_out_of_order a [] = raise Noassoc
    5.28  |   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
    5.29  
    5.30  fun get_assoc_snds [] xs assocs= assocs
    5.31 @@ -180,7 +179,7 @@
    5.32                                              (* literals of -all- axioms, not just those used by spass *)
    5.33                                              val meta_strs = map get_meta_lits metas
    5.34                                             
    5.35 -                                            val metas_and_strs = zip  metas meta_strs
    5.36 +                                            val metas_and_strs = ListPair.zip (metas,meta_strs)
    5.37                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    5.38                                               val _ = TextIO.output (outfile, onestr ax_strs)
    5.39                                               
    5.40 @@ -193,14 +192,14 @@
    5.41  
    5.42                                              val ax_metas = get_assoc_snds ax_strs metas_and_strs []
    5.43                                              val ax_vars = map thm_vars ax_metas
    5.44 -                                            val ax_with_vars = zip ax_metas ax_vars
    5.45 +                                            val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
    5.46  
    5.47                                              (* get list of extra axioms as thms with their variables *)
    5.48                                              val extra_metas = add_if_not_inlist metas ax_metas []
    5.49                                              val extra_vars = map thm_vars extra_metas
    5.50                                              val extra_with_vars = if (not (extra_metas = []) ) 
    5.51                                                                    then
    5.52 - 									 zip extra_metas extra_vars
    5.53 + 									 ListPair.zip (extra_metas,extra_vars)
    5.54                                                                    else
    5.55                                                                           []
    5.56  
    5.57 @@ -218,7 +217,7 @@
    5.58                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    5.59                                             
    5.60                                           in
    5.61 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas))
    5.62 +                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
    5.63                                           end
    5.64                                          
    5.65  fun thmstrings [] str = str
    5.66 @@ -347,12 +346,12 @@
    5.67                                                    (* do the bit for the Isabelle ordered axioms at the top *)
    5.68                                                    val ax_nums = map #1 numcls
    5.69                                                    val ax_strs = map get_meta_lits_bracket (map #2 numcls)
    5.70 -                                                  val numcls_strs = zip ax_nums ax_strs
    5.71 +                                                  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
    5.72                                                    val num_cls_vars =  map (addvars vars) numcls_strs;
    5.73 -                                                  val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
    5.74 +                                                  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
    5.75                                                    
    5.76                                                    val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
    5.77 -                                                  val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
    5.78 +                                                  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
    5.79                                                    val frees_str = "["^(thmvars_to_string frees "")^"]"
    5.80                                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
    5.81  
    5.82 @@ -640,15 +639,15 @@
    5.83  
    5.84  fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
    5.85                             val extraax_num = length extraaxioms
    5.86 -                           val origaxioms_and_steps = drop (extraax_num) xs  
    5.87 +                           val origaxioms_and_steps = Library.drop (extraax_num, xs)  
    5.88                            
    5.89    
    5.90                             val origaxioms = get_origaxioms origaxioms_and_steps
    5.91                             val origax_num = length origaxioms
    5.92 -                           val axioms_and_steps = drop (origax_num + extraax_num) xs  
    5.93 +                           val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
    5.94                             val axioms = get_axioms axioms_and_steps
    5.95                             
    5.96 -                           val steps = drop origax_num axioms_and_steps
    5.97 +                           val steps = Library.drop (origax_num, axioms_and_steps)
    5.98                             val firststeps = butlast steps
    5.99                             val laststep = last steps
   5.100                             val goalstring = implode(butlast(explode goalstring))
     6.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 19 15:15:06 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 19 18:08:44 2005 +0200
     6.3 @@ -62,18 +62,20 @@
     6.4                                   implode(List.filter is_alpha_space_digit_or_neg exp_term)
     6.5                               end
     6.6  
     6.7 +fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
     6.8  
     6.9  (****************************************)
    6.10  (* Reconstruct an axiom resolution step *)
    6.11  (****************************************)
    6.12  
    6.13 - fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    6.14 -                                     let val this_axiom =(Recon_Base.assoc  clausenum clauses)
    6.15 +fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    6.16 +                                     let val this_axiom = valOf (assoc (clauses,clausenum))
    6.17                                           val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
    6.18                                           val thmvars = thm_vars res
    6.19                                       in
    6.20                                           (res, (Axiom,clause_strs,thmvars )  )
    6.21                                       end
    6.22 +                                     handle Option => reconstruction_failed "follow_axiom"
    6.23  
    6.24  (****************************************)
    6.25  (* Reconstruct a binary resolution step *)
    6.26 @@ -82,14 +84,15 @@
    6.27                   (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
    6.28  fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
    6.29          = let
    6.30 -              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
    6.31 -              val thm2 =  Recon_Base.assoc  clause2 thml
    6.32 +              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    6.33 +              val thm2 =  valOf (assoc (thml,clause2))
    6.34                val res =   thm1 RSN ((lit2 +1), thm2)
    6.35                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    6.36                val thmvars = thm_vars res
    6.37            in
    6.38               (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
    6.39            end
    6.40 +	  handle Option => reconstruction_failed "follow_binary"
    6.41  
    6.42  
    6.43  
    6.44 @@ -100,14 +103,15 @@
    6.45  
    6.46  fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
    6.47          = let
    6.48 -              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
    6.49 -              val thm2 =  Recon_Base.assoc  clause2 thml
    6.50 +              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    6.51 +              val thm2 =  valOf (assoc (thml,clause2))
    6.52                val res =   thm1 RSN ((lit2 +1), thm2)
    6.53                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    6.54                val thmvars = thm_vars res
    6.55            in
    6.56               (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
    6.57            end
    6.58 +	  handle Option => reconstruction_failed "follow_mrr"
    6.59  
    6.60  
    6.61  (*******************************************)
    6.62 @@ -144,7 +148,7 @@
    6.63  (*FIXME: share code with that in Tools/reconstruction.ML*)
    6.64  fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
    6.65                            let 
    6.66 -                            val th =  Recon_Base.assoc clause thml
    6.67 +                            val th =  valOf (assoc (thml,clause))
    6.68                              val prems = prems_of th
    6.69                              val sign = sign_of_thm th
    6.70                              val fac1 = get_nth (lit1+1) prems
    6.71 @@ -178,15 +182,8 @@
    6.72                                  in 
    6.73                                         (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
    6.74                                  end
    6.75 -                         end;
    6.76 -
    6.77 -
    6.78 -
    6.79 -Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
    6.80 -val prems = it;
    6.81 -br (hd prems) 1;
    6.82 -br (hd(tl(tl prems))) 1;
    6.83 -qed "merge";
    6.84 +                         end
    6.85 +                         handle Option => reconstruction_failed "follow_factor"
    6.86  
    6.87  
    6.88  
    6.89 @@ -217,8 +214,8 @@
    6.90  
    6.91  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
    6.92                            let 
    6.93 -                            val th1 =  Recon_Base.assoc clause1 thml
    6.94 -                            val th2 =  Recon_Base.assoc clause2 thml 
    6.95 +                            val th1 =  valOf (assoc (thml,clause1))
    6.96 +                            val th2 =  valOf (assoc (thml,clause2)) 
    6.97                              val eq_lit_th = select_literal (lit1+1) th1
    6.98                              val mod_lit_th = select_literal (lit2+1) th2
    6.99                              val eqsubst = eq_lit_th RSN (2,rev_subst)
   6.100 @@ -236,12 +233,13 @@
   6.101                           in 
   6.102                             (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   6.103                           end
   6.104 +			 handle Option => reconstruction_failed "follow_standard_para"
   6.105  
   6.106  (*              
   6.107  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
   6.108                            let 
   6.109 -                            val th1 =  Recon_Base.assoc clause1 thml
   6.110 -                            val th2 =  Recon_Base.assoc clause2 thml 
   6.111 +                            val th1 =  valOf (assoc (thml,clause1))
   6.112 +                            val th2 =  valOf (assoc (thml,clause2)) 
   6.113                              val eq_lit_th = select_literal (lit1+1) th1
   6.114                              val mod_lit_th = select_literal (lit2+1) th2
   6.115                              val eqsubst = eq_lit_th RSN (2,rev_subst)
   6.116 @@ -252,6 +250,7 @@
   6.117                           in 
   6.118                             (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   6.119                           end
   6.120 +			 handle Option => reconstruction_failed "follow_standard_para"
   6.121  
   6.122  *)
   6.123  
   6.124 @@ -292,8 +291,8 @@
   6.125                      (* clause1, lit1 is thing to rewrite with *)
   6.126  fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
   6.127  
   6.128 -                          let val th1 =  Recon_Base.assoc clause1 thml
   6.129 -                              val th2 = Recon_Base.assoc clause2 thml
   6.130 +                          let val th1 =  valOf (assoc (thml,clause1))
   6.131 +                              val th2 = valOf (assoc (thml,clause2))
   6.132                                val eq_lit_th = select_literal (lit1+1) th1
   6.133                                val mod_lit_th = select_literal (lit2+1) th2
   6.134                                val eqsubst = eq_lit_th RSN (2,rev_subst)
   6.135 @@ -309,6 +308,7 @@
   6.136                             in
   6.137                                 (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
   6.138                             end
   6.139 +			   handle Option => reconstruction_failed "follow_rewrite"
   6.140  
   6.141  
   6.142  
   6.143 @@ -318,7 +318,7 @@
   6.144  
   6.145  
   6.146  fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
   6.147 -                           let val th1 =  Recon_Base.assoc clause1 thml
   6.148 +                           let val th1 =  valOf (assoc (thml,clause1))
   6.149                                 val prems1 = prems_of th1
   6.150                                 val newthm = refl RSN ((lit1+ 1), th1)
   6.151                                                 handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   6.152 @@ -327,6 +327,7 @@
   6.153                             in 
   6.154                                 (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
   6.155                             end
   6.156 +  	 		   handle Option => reconstruction_failed "follow_obvious"
   6.157  
   6.158  (**************************************************************************************)
   6.159  (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
     7.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 19 15:15:06 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 19 18:08:44 2005 +0200
     7.3 @@ -32,7 +32,7 @@
     7.4                                                val numbers = 0 upto (num_of_cls -1)
     7.5                                                val multi_name = multi name num_of_cls []
     7.6                                            in 
     7.7 -                                              zip multi_name numbers
     7.8 +                                              ListPair.zip (multi_name,numbers)
     7.9                                            end;
    7.10  
    7.11  fun stick []  = []
    7.12 @@ -108,7 +108,7 @@
    7.13                                      (* get (name, thm) pairs for claset rules *)
    7.14                                     (*******************************************)
    7.15  
    7.16 -                                   val names_rules = zip good_names name_fol_cs;
    7.17 +                                   val names_rules = ListPair.zip (good_names,name_fol_cs);
    7.18                                     
    7.19                                     val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
    7.20  
    7.21 @@ -118,7 +118,7 @@
    7.22                                     val stick_clasrls =  map stick claset_tptp_strs;
    7.23                                     (* stick stick_clasrls length is 172*)
    7.24  
    7.25 -                                   val name_stick = zip good_names stick_clasrls;
    7.26 +                                   val name_stick = ListPair.zip (good_names,stick_clasrls);
    7.27  
    7.28                                     val cl_name_nums =map clause_numbering name_stick;
    7.29                                         
    7.30 @@ -169,7 +169,7 @@
    7.31                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    7.32  
    7.33                                      val stick_strs = map stick simpset_tptp_strs;
    7.34 -                                    val name_stick = zip simp_names stick_strs;
    7.35 +                                    val name_stick = ListPair.zip (simp_names,stick_strs);
    7.36  
    7.37                                      val name_nums =map clause_numbering name_stick;
    7.38                                      (* length 2409*)
     8.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Apr 19 15:15:06 2005 +0200
     8.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Apr 19 18:08:44 2005 +0200
     8.3 @@ -605,7 +605,7 @@
     8.4  
     8.5                                                            let val thm = thm_of_string thmstring
     8.6                                                                val clauses = make_clauses [thm]
     8.7 -                                                              val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
     8.8 +                                                              val numcls =  ListPair.zip  (numlist (length clauses), map make_meta_clause clauses)
     8.9                                                           
    8.10                                                            in
    8.11                                                               Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
     9.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 19 15:15:06 2005 +0200
     9.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 19 18:08:44 2005 +0200
     9.3 @@ -104,7 +104,7 @@
     9.4          val prems'' = make_clauses prems'
     9.5          val prems''' = ResAxioms.rm_Eps [] prems''
     9.6          val clss = map ResClause.make_conjecture_clause prems'''
     9.7 -	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss) 
     9.8 +	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
     9.9  	val tfree_lits = ResLib.flat_noDup tfree_litss
    9.10  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    9.11          val hypsfile = File.sysify_path hyps_file
    9.12 @@ -123,7 +123,7 @@
    9.13      let val _ = (warning ("in tptp_inputs_tfrees 0"))
    9.14          val clss = map (ResClause.make_conjecture_clause_thm) thms
    9.15           val _ = (warning ("in tptp_inputs_tfrees 1"))
    9.16 -	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
    9.17 +	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    9.18          val _ = (warning ("in tptp_inputs_tfrees 2"))
    9.19  	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    9.20           val _ = (warning ("in tptp_inputs_tfrees 3"))
    10.1 --- a/src/HOL/Tools/res_clause.ML	Tue Apr 19 15:15:06 2005 +0200
    10.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Apr 19 18:08:44 2005 +0200
    10.3 @@ -212,7 +212,7 @@
    10.4  fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) 
    10.5    | type_of (Type (a, Ts)) = 
    10.6      let val foltyps_ts = map type_of Ts
    10.7 -        val (folTyps,ts) = ResLib.unzip foltyps_ts
    10.8 +        val (folTyps,ts) = ListPair.unzip foltyps_ts
    10.9          val ts' = ResLib.flat_noDup ts
   10.10      in    
   10.11          (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)),ts') 
   10.12 @@ -279,14 +279,14 @@
   10.13      let val (f,args) = strip_comb app
   10.14          fun term_of_aux () = 
   10.15              let val (funName,(funType,ts1)) = fun_name_type f
   10.16 -                 val (args',ts2) = ResLib.unzip (map term_of args)
   10.17 +                 val (args',ts2) = ListPair.unzip (map term_of args)
   10.18                   val ts3 = ResLib.flat_noDup (ts1::ts2)
   10.19              in
   10.20  		(Fun(funName,funType,args'),ts3)
   10.21              end
   10.22  	fun term_of_eq ((Const ("op =", typ)),args) =
   10.23  	    let val arg_typ = eq_arg_type typ
   10.24 -		val (args',ts) = ResLib.unzip (map term_of args)
   10.25 +		val (args',ts) = ListPair.unzip (map term_of args)
   10.26  		val equal_name = lookup_const ("op =")
   10.27  	    in
   10.28  		(Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
   10.29 @@ -304,7 +304,7 @@
   10.30  
   10.31  fun pred_of_eq ((Const ("op =", typ)),args) =
   10.32      let val arg_typ = eq_arg_type typ 
   10.33 -	val (args',ts) = ResLib.unzip (map term_of args)
   10.34 +	val (args',ts) = ListPair.unzip (map term_of args)
   10.35  	val equal_name = lookup_const "op ="
   10.36      in
   10.37  	(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
   10.38 @@ -315,7 +315,7 @@
   10.39  (* The input "pred" cannot be an equality *)
   10.40  fun pred_of_nonEq (pred,args) = 
   10.41      let val (predName,(predType,ts1)) = pred_name_type pred
   10.42 -	val (args',ts2) = ResLib.unzip (map term_of args)
   10.43 +	val (args',ts2) = ListPair.unzip (map term_of args)
   10.44  	val ts3 = ResLib.flat_noDup (ts1::ts2)
   10.45      in
   10.46  	(Predicate(predName,predType,args'),ts3)
   10.47 @@ -507,7 +507,7 @@
   10.48  	 val nargs = length args
   10.49  	 val tvars = get_TVars nargs
   10.50  	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
   10.51 -         val tvars_srts = ResLib.zip tvars args
   10.52 +         val tvars_srts = ListPair.zip (tvars,args)
   10.53  	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
   10.54           val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
   10.55  	 val premLits = map make_TVarLit false_tvars_srts'
    11.1 --- a/src/HOL/Tools/res_lib.ML	Tue Apr 19 15:15:06 2005 +0200
    11.2 +++ b/src/HOL/Tools/res_lib.ML	Tue Apr 19 18:08:44 2005 +0200
    11.3 @@ -22,10 +22,8 @@
    11.4  	val no_rep_app : ''a list -> ''a list -> ''a list
    11.5  	val pair_ins : 'a -> 'b list -> ('a * 'b) list
    11.6  	val rm_rep : ''a list -> ''a list
    11.7 -	val unzip : ('a * 'b) list -> 'a list * 'b list
    11.8  	val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    11.9  	val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
   11.10 -	val zip : 'a list -> 'b list -> ('a * 'b) list
   11.11  
   11.12  end;
   11.13  
   11.14 @@ -80,18 +78,6 @@
   11.15  	fun rm_rep []     = []
   11.16  	  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
   11.17  
   11.18 -	fun unzip []             =
   11.19 -		([], [])
   11.20 -	  | unzip ((x1, y1)::zs) =
   11.21 -		let
   11.22 -			val (xs, ys) = unzip zs
   11.23 -		in
   11.24 -			(x1::xs, y1::ys)
   11.25 -		end;
   11.26 -
   11.27 -	fun zip []      []      = []
   11.28 -	  | zip (x::xs) (y::ys) = (x, y)::(zip xs ys);
   11.29 -
   11.30  	fun flat_noDup []     = []
   11.31  	  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
   11.32