# HG changeset patch # User paulson # Date 1113926924 -7200 # Node ID 9df37a0e935d66bbd07fbd4968899b10091f1041 # Parent f14ae24327100ecf1df3b9cc6380b1635ea8eac4 more tidying of libraries in Reconstruction diff -r f14ae2432710 -r 9df37a0e935d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 19 18:08:44 2005 +0200 @@ -114,10 +114,10 @@ blastdata.ML cladata.ML \ Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ Tools/res_axioms.ML Tools/res_types_sorts.ML \ - Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\ + Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\ Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \ Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \ - Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ + Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ document/root.tex hologic.ML simpdata.ML thy_syntax.ML @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Reconstruction.thy Tue Apr 19 18:08:44 2005 +0200 @@ -15,7 +15,6 @@ "Tools/res_types_sorts.ML" "Tools/ATP/recon_prelim.ML" - "Tools/ATP/recon_gandalf_base.ML" "Tools/ATP/recon_order_clauses.ML" "Tools/ATP/recon_translate_proof.ML" "Tools/ATP/recon_parse.ML" diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/recon_gandalf_base.ML --- a/src/HOL/Tools/ATP/recon_gandalf_base.ML Tue Apr 19 15:15:06 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -structure Recon_Base = -struct - -(* Auxiliary functions *) - -exception Assertion of string; - -val DEBUG = ref true; -fun TRACE s = if !DEBUG then print s else (); - -exception Noassoc; -fun assoc a [] = raise Noassoc - | assoc a ((x, y)::t) = if a = x then y else assoc a t; -fun assoc_exists a [] = false - | assoc_exists a ((x, y)::t) = if a = x then true else assoc_exists a t; -fun assoc_update (a, b) [] = raise Noassoc - | assoc_update (a, b) ((x, y)::t) - = if a = x then (a, b)::t else (x, y)::(assoc_update (a, b) t) -fun assoc_inv a [] = raise Noassoc - | assoc_inv a ((x, y)::t) = if a = y then x else assoc a t; -fun assoc_inv_exists a [] = false - | assoc_inv_exists a ((x, y)::t) = if a = y then true else assoc_inv_exists a t; - -fun is_mem x [] = false - | is_mem x (h::t) = (x = h) orelse is_mem x t; -fun elt 0 (h::t) = h - | elt n (h::t) = elt (n - 1) t - | elt n l = raise (Assertion "elt: out of range"); -fun remove_elt _ [] = raise (Assertion "remove_elt: out of range") - | remove_elt 0 (h::t) = t - | remove_elt n (h::t) = h::(remove_elt (n - 1) t); -fun elt_num x [] = raise (Assertion "elt_num: not in list") - | elt_num x (h::t) = if h = x then 0 else 1 + elt_num x t; -fun set_add x l = if is_mem x l then l else x::l; - -fun iter f a [] = a - | iter f a (h::t) = f h (iter f a t); - -end; diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 19 18:08:44 2005 +0200 @@ -2,27 +2,16 @@ (* Reorder clauses for use in binary resolution *) (*----------------------------------------------*) -fun drop n [] = [] -| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) - fun remove_nth n [] = [] | remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n)) -fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) +(*Differs from List.nth: it counts from 1 rather than from 0*) +fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs)) exception Not_in_list; -fun zip xs [] = [] -| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys)) - - -fun unzip [] = ([],[]) - | unzip((x,y)::pairs) = - let val (xs,ys) = unzip pairs - in (x::xs, y::ys) end; - fun numlist 0 = [] | numlist n = (numlist (n - 1))@[n] @@ -39,13 +28,6 @@ (* code to rearrange clauses so that they're the same as the parsed in SPASS version *) -fun assoc3 a [] = raise Recon_Base.Noassoc - | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t; - - -fun third (a,b,c) = c; - - fun takeUntil ch [] res = (res, []) | takeUntil ch (x::xs) res = if x = ch then @@ -70,12 +52,12 @@ then let val (left, right) = takeUntil "=" str [] in - ((butlast left), (drop 1 right)) + (butlast left, tl right) end else (* is an inequality *) let val (left, right) = takeUntil "~" str [] in - ((butlast left), (drop 2 right)) + (butlast left, tl (tl right)) end @@ -101,23 +83,16 @@ -fun var_pos_eq vars x y = let val xs = explode x +fun var_pos_eq vars x y = String.size x = String.size y andalso + let val xs = explode x val ys = explode y + val xsys = ListPair.zip (xs,ys) + val are_var_pairs = map (var_equiv vars) xsys in - if not_equal (length xs) (length ys) - then - false - else - let val xsys = zip xs ys - val are_var_pairs = map (var_equiv vars) xsys - in - all_true are_var_pairs - end + all_true are_var_pairs end - - fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = let val y = explode x diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 19 18:08:44 2005 +0200 @@ -116,7 +116,9 @@ fun get_step_nums [] nums = nums | get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num]) -fun assoc_snd a [] = raise Recon_Base.Noassoc +exception Noassoc; + +fun assoc_snd a [] = raise Noassoc | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t; (* change to be something using check_order instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *) @@ -125,13 +127,10 @@ | get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))]) *) (*FIX - should this have vars in it? *) -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) - in - true - end - handle EXCEP => false +fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) + handle _ => false -fun assoc_out_of_order a [] = raise Recon_Base.Noassoc +fun assoc_out_of_order a [] = raise Noassoc | assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t; fun get_assoc_snds [] xs assocs= assocs @@ -180,7 +179,7 @@ (* literals of -all- axioms, not just those used by spass *) val meta_strs = map get_meta_lits metas - val metas_and_strs = zip metas meta_strs + val metas_and_strs = ListPair.zip (metas,meta_strs) val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses"))); val _ = TextIO.output (outfile, onestr ax_strs) @@ -193,14 +192,14 @@ val ax_metas = get_assoc_snds ax_strs metas_and_strs [] val ax_vars = map thm_vars ax_metas - val ax_with_vars = zip ax_metas ax_vars + val ax_with_vars = ListPair.zip (ax_metas,ax_vars) (* get list of extra axioms as thms with their variables *) val extra_metas = add_if_not_inlist metas ax_metas [] val extra_vars = map thm_vars extra_metas val extra_with_vars = if (not (extra_metas = []) ) then - zip extra_metas extra_vars + ListPair.zip (extra_metas,extra_vars) else [] @@ -218,7 +217,7 @@ val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) in - (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas)) + (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas))) end fun thmstrings [] str = str @@ -347,12 +346,12 @@ (* do the bit for the Isabelle ordered axioms at the top *) val ax_nums = map #1 numcls val ax_strs = map get_meta_lits_bracket (map #2 numcls) - val numcls_strs = zip ax_nums ax_strs + val numcls_strs = ListPair.zip (ax_nums,ax_strs) val num_cls_vars = map (addvars vars) numcls_strs; - val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) "" + val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) "" val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else [] - val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) "" + val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" val frees_str = "["^(thmvars_to_string frees "")^"]" val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile"))); @@ -640,15 +639,15 @@ fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs val extraax_num = length extraaxioms - val origaxioms_and_steps = drop (extraax_num) xs + val origaxioms_and_steps = Library.drop (extraax_num, xs) val origaxioms = get_origaxioms origaxioms_and_steps val origax_num = length origaxioms - val axioms_and_steps = drop (origax_num + extraax_num) xs + val axioms_and_steps = Library.drop (origax_num + extraax_num, xs) val axioms = get_axioms axioms_and_steps - val steps = drop origax_num axioms_and_steps + val steps = Library.drop (origax_num, axioms_and_steps) val firststeps = butlast steps val laststep = last steps val goalstring = implode(butlast(explode goalstring)) diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 19 18:08:44 2005 +0200 @@ -62,18 +62,20 @@ implode(List.filter is_alpha_space_digit_or_neg exp_term) end +fun reconstruction_failed fname = error (fname ^ ": reconstruction failed") (****************************************) (* Reconstruct an axiom resolution step *) (****************************************) - fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = - let val this_axiom =(Recon_Base.assoc clausenum clauses) +fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = + let val this_axiom = valOf (assoc (clauses,clausenum)) val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars) val thmvars = thm_vars res in (res, (Axiom,clause_strs,thmvars ) ) end + handle Option => reconstruction_failed "follow_axiom" (****************************************) (* Reconstruct a binary resolution step *) @@ -82,14 +84,15 @@ (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *) fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = let - val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml) - val thm2 = Recon_Base.assoc clause2 thml + val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) + val thm2 = valOf (assoc (thml,clause2)) val res = thm1 RSN ((lit2 +1), thm2) val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) val thmvars = thm_vars res in (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) end + handle Option => reconstruction_failed "follow_binary" @@ -100,14 +103,15 @@ fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = let - val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml) - val thm2 = Recon_Base.assoc clause2 thml + val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) + val thm2 = valOf (assoc (thml,clause2)) val res = thm1 RSN ((lit2 +1), thm2) val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) val thmvars = thm_vars res in (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) end + handle Option => reconstruction_failed "follow_mrr" (*******************************************) @@ -144,7 +148,7 @@ (*FIXME: share code with that in Tools/reconstruction.ML*) fun follow_factor clause lit1 lit2 allvars thml clause_strs= let - val th = Recon_Base.assoc clause thml + val th = valOf (assoc (thml,clause)) val prems = prems_of th val sign = sign_of_thm th val fac1 = get_nth (lit1+1) prems @@ -178,15 +182,8 @@ in (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) end - end; - - - -Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False"; -val prems = it; -br (hd prems) 1; -br (hd(tl(tl prems))) 1; -qed "merge"; + end + handle Option => reconstruction_failed "follow_factor" @@ -217,8 +214,8 @@ fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= let - val th1 = Recon_Base.assoc clause1 thml - val th2 = Recon_Base.assoc clause2 thml + val th1 = valOf (assoc (thml,clause1)) + val th2 = valOf (assoc (thml,clause2)) val eq_lit_th = select_literal (lit1+1) th1 val mod_lit_th = select_literal (lit2+1) th2 val eqsubst = eq_lit_th RSN (2,rev_subst) @@ -236,12 +233,13 @@ in (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) end + handle Option => reconstruction_failed "follow_standard_para" (* fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= let - val th1 = Recon_Base.assoc clause1 thml - val th2 = Recon_Base.assoc clause2 thml + val th1 = valOf (assoc (thml,clause1)) + val th2 = valOf (assoc (thml,clause2)) val eq_lit_th = select_literal (lit1+1) th1 val mod_lit_th = select_literal (lit2+1) th2 val eqsubst = eq_lit_th RSN (2,rev_subst) @@ -252,6 +250,7 @@ in (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) end + handle Option => reconstruction_failed "follow_standard_para" *) @@ -292,8 +291,8 @@ (* clause1, lit1 is thing to rewrite with *) fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= - let val th1 = Recon_Base.assoc clause1 thml - val th2 = Recon_Base.assoc clause2 thml + let val th1 = valOf (assoc (thml,clause1)) + val th2 = valOf (assoc (thml,clause2)) val eq_lit_th = select_literal (lit1+1) th1 val mod_lit_th = select_literal (lit2+1) th2 val eqsubst = eq_lit_th RSN (2,rev_subst) @@ -309,6 +308,7 @@ in (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) end + handle Option => reconstruction_failed "follow_rewrite" @@ -318,7 +318,7 @@ fun follow_obvious (clause1, lit1) allvars thml clause_strs= - let val th1 = Recon_Base.assoc clause1 thml + let val th1 = valOf (assoc (thml,clause1)) val prems1 = prems_of th1 val newthm = refl RSN ((lit1+ 1), th1) handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) @@ -327,6 +327,7 @@ in (res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) end + handle Option => reconstruction_failed "follow_obvious" (**************************************************************************************) (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*) diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 19 18:08:44 2005 +0200 @@ -32,7 +32,7 @@ val numbers = 0 upto (num_of_cls -1) val multi_name = multi name num_of_cls [] in - zip multi_name numbers + ListPair.zip (multi_name,numbers) end; fun stick [] = [] @@ -108,7 +108,7 @@ (* get (name, thm) pairs for claset rules *) (*******************************************) - val names_rules = zip good_names name_fol_cs; + val names_rules = ListPair.zip (good_names,name_fol_cs); val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[]) @@ -118,7 +118,7 @@ val stick_clasrls = map stick claset_tptp_strs; (* stick stick_clasrls length is 172*) - val name_stick = zip good_names stick_clasrls; + val name_stick = ListPair.zip (good_names,stick_clasrls); val cl_name_nums =map clause_numbering name_stick; @@ -169,7 +169,7 @@ val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps; val stick_strs = map stick simpset_tptp_strs; - val name_stick = zip simp_names stick_strs; + val name_stick = ListPair.zip (simp_names,stick_strs); val name_nums =map clause_numbering name_stick; (* length 2409*) diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Tue Apr 19 18:08:44 2005 +0200 @@ -605,7 +605,7 @@ let val thm = thm_of_string thmstring val clauses = make_clauses [thm] - val numcls = zip (numlist (length clauses)) (map make_meta_clause clauses) + val numcls = ListPair.zip (numlist (length clauses), map make_meta_clause clauses) in Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/res_atp.ML --- 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")) diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Tue Apr 19 18:08:44 2005 +0200 @@ -212,7 +212,7 @@ fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) | type_of (Type (a, Ts)) = let val foltyps_ts = map type_of Ts - val (folTyps,ts) = ResLib.unzip foltyps_ts + val (folTyps,ts) = ListPair.unzip foltyps_ts val ts' = ResLib.flat_noDup ts in (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)),ts') @@ -279,14 +279,14 @@ let val (f,args) = strip_comb app fun term_of_aux () = let val (funName,(funType,ts1)) = fun_name_type f - val (args',ts2) = ResLib.unzip (map term_of args) + val (args',ts2) = ListPair.unzip (map term_of args) val ts3 = ResLib.flat_noDup (ts1::ts2) in (Fun(funName,funType,args'),ts3) end fun term_of_eq ((Const ("op =", typ)),args) = let val arg_typ = eq_arg_type typ - val (args',ts) = ResLib.unzip (map term_of args) + val (args',ts) = ListPair.unzip (map term_of args) val equal_name = lookup_const ("op =") in (Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts) @@ -304,7 +304,7 @@ fun pred_of_eq ((Const ("op =", typ)),args) = let val arg_typ = eq_arg_type typ - val (args',ts) = ResLib.unzip (map term_of args) + val (args',ts) = ListPair.unzip (map term_of args) val equal_name = lookup_const "op =" in (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts) @@ -315,7 +315,7 @@ (* The input "pred" cannot be an equality *) fun pred_of_nonEq (pred,args) = let val (predName,(predType,ts1)) = pred_name_type pred - val (args',ts2) = ResLib.unzip (map term_of args) + val (args',ts2) = ListPair.unzip (map term_of args) val ts3 = ResLib.flat_noDup (ts1::ts2) in (Predicate(predName,predType,args'),ts3) @@ -507,7 +507,7 @@ val nargs = length args val tvars = get_TVars nargs val conclLit = make_TConsLit(true,(res,tcons,tvars)) - val tvars_srts = ResLib.zip tvars args + val tvars_srts = ListPair.zip (tvars,args) val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) val false_tvars_srts' = ResLib.pair_ins false tvars_srts' val premLits = map make_TVarLit false_tvars_srts' diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/res_lib.ML --- a/src/HOL/Tools/res_lib.ML Tue Apr 19 15:15:06 2005 +0200 +++ b/src/HOL/Tools/res_lib.ML Tue Apr 19 18:08:44 2005 +0200 @@ -22,10 +22,8 @@ val no_rep_app : ''a list -> ''a list -> ''a list val pair_ins : 'a -> 'b list -> ('a * 'b) list val rm_rep : ''a list -> ''a list - val unzip : ('a * 'b) list -> 'a list * 'b list val write_strs : TextIO.outstream -> TextIO.vector list -> unit val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit - val zip : 'a list -> 'b list -> ('a * 'b) list end; @@ -80,18 +78,6 @@ fun rm_rep [] = [] | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y); - fun unzip [] = - ([], []) - | unzip ((x1, y1)::zs) = - let - val (xs, ys) = unzip zs - in - (x1::xs, y1::ys) - end; - - fun zip [] [] = [] - | zip (x::xs) (y::ys) = (x, y)::(zip xs ys); - fun flat_noDup [] = [] | flat_noDup (x::y) = no_rep_app x (flat_noDup y);