# HG changeset patch # User wenzelm # Date 1256680574 -3600 # Node ID 65232054ffd01f074f9c13bc632fc0fc11456977 # Parent db230399f8900c0050adb5ff3e3735aca09b1f73 eliminated some old folds; diff -r db230399f890 -r 65232054ffd0 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/FOLP/simp.ML Tue Oct 27 22:56:14 2009 +0100 @@ -254,13 +254,13 @@ val insert_thms = fold_rev insert_thm_warn; -fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = +fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let val thms = mk_simps thm in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} end; -val op addrews = Library.foldl addrew; +fun ss addrews thms = fold addrew thms ss; fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = thms @ congs; @@ -287,7 +287,7 @@ mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} end; -fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = +fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let fun find((p as (th,ths))::ps',ps) = if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) | find([],simps') = @@ -298,7 +298,7 @@ simps = simps', simp_net = delete_thms thms simp_net } end; -val op delrews = Library.foldl delrew; +fun ss delrews thms = fold delrew thms ss; fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = diff -r db230399f890 -r 65232054ffd0 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Import/shuffler.ML Tue Oct 27 22:56:14 2009 +0100 @@ -248,16 +248,16 @@ val tvars = OldTerm.term_tvars t val tfree_names = OldTerm.add_term_tfree_names(t,[]) val (type_inst,_) = - Library.foldl (fn ((inst,used),(w as (v,_),S)) => + fold (fn (w as (v,_), S) => fn (inst, used) => let val v' = Name.variant used v in ((w,TFree(v',S))::inst,v'::used) end) - (([],tfree_names),tvars) + tvars ([], tfree_names) val t' = subst_TVars type_inst t in - (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S)) + (t', map (fn (w,TFree(v,S)) => (v,TVar(w,S)) | _ => error "Internal error in Shuffler.freeze_thaw") type_inst) end diff -r db230399f890 -r 65232054ffd0 src/HOL/Matrix/cplex/CplexMatrixConverter.ML --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Tue Oct 27 22:56:14 2009 +0100 @@ -75,7 +75,7 @@ set_elem vec (s2i v) (if positive then num else "-"^num) | setprod _ _ _ = raise (Converter "term is not a normed product") - fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts) + fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector | sum2vec t = setprod empty_vector true t fun constrs2Ab j A b [] = (A, b) @@ -100,9 +100,9 @@ fun convert_results (cplex.Optimal (opt, entries)) name2index = let - fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value) + fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value in - (opt, Library.foldl setv (matrix_builder.empty_vector, entries)) + (opt, fold setv entries (matrix_builder.empty_vector)) end | convert_results _ _ = raise (Converter "No optimal result") diff -r db230399f890 -r 65232054ffd0 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Tue Oct 27 22:56:14 2009 +0100 @@ -189,12 +189,11 @@ in fun derive_init_eqs sgn rules eqs = let - val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) - eqs - fun countlist l = - (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) + val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) eqs + fun countlist l = + rev (snd (fold (fn e => fn (i, L) => (i + 1, (e, i) :: L)) l (0, []))) in - maps (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths) + maps (fn (e, i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths) end; end; diff -r db230399f890 -r 65232054ffd0 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Tools/choice_specification.ML Tue Oct 27 22:56:14 2009 +0100 @@ -165,7 +165,7 @@ val cnames = map (fst o dest_Const) proc_consts fun post_process (arg as (thy,thm)) = let - fun inst_all thy (thm,v) = + fun inst_all thy v thm = let val cv = cterm_of thy v val cT = ctyp_of_term cv @@ -174,7 +174,7 @@ thm RS spec' end fun remove_alls frees thm = - Library.foldl (inst_all (Thm.theory_of_thm thm)) (thm,frees) + fold (inst_all (Thm.theory_of_thm thm)) frees thm fun process_single ((name,atts),rew_imp,frees) args = let fun undo_imps thm = diff -r db230399f890 -r 65232054ffd0 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Tools/hologic.ML Tue Oct 27 22:56:14 2009 +0100 @@ -638,8 +638,8 @@ val Ts = map snd vs; val t = Const (c, Ts ---> T); val tt = mk_prod (t, Abs ("u", unitT, reflect_term t)); - fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T); - in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end; + fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T); + in fold app (mk_fTs Ts T ~~ vs) tt end; (* open state monads *) diff -r db230399f890 -r 65232054ffd0 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOL/Tools/meson.ML Tue Oct 27 22:56:14 2009 +0100 @@ -462,14 +462,13 @@ (** Detecting repeated assumptions in a subgoal **) (*The stringtree detects repeated assumptions.*) -fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net; +fun ins_term t net = Net.insert_term (op aconv) (t, t) net; (*detects repetitions in a list of terms*) fun has_reps [] = false | has_reps [_] = false | has_reps [t,u] = (t aconv u) - | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) - handle Net.INSERT => true; + | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) fun TRYING_eq_assume_tac 0 st = Seq.single st diff -r db230399f890 -r 65232054ffd0 src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOLCF/IOA/ABP/Check.ML Tue Oct 27 22:56:14 2009 +0100 @@ -15,8 +15,8 @@ fun check(extacts,intacts,string_of_a,startsI,string_of_s, nexts,hom,transA,startsS) = let fun check_s(s,unchecked,checked) = - let fun check_sa(unchecked,a) = - let fun check_sas(unchecked,t) = + let fun check_sa a unchecked = + let fun check_sas t unchecked = (if a mem extacts then (if transA(hom s,a,hom t) then ( ) else (writeln("Error: Mapping of Externals!"); @@ -29,8 +29,8 @@ string_of_a a; writeln""; string_of_s t;writeln"";writeln"" )); if t mem checked then unchecked else insert (op =) t unchecked) - in Library.foldl check_sas (unchecked,nexts s a) end; - val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts) + in fold check_sas (nexts s a) unchecked end; + val unchecked' = fold check_sa (extacts @ intacts) unchecked in (if s mem startsI then (if hom(s) mem startsS then () else writeln("Error: At start states!")) diff -r db230399f890 -r 65232054ffd0 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Oct 27 22:56:14 2009 +0100 @@ -17,7 +17,7 @@ end; -structure Domain_Axioms :> DOMAIN_AXIOMS = +structure Domain_Axioms : DOMAIN_AXIOMS = struct open Domain_Library; @@ -218,13 +218,13 @@ ("bisim_def", %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); - fun add_one (thy,(dnam,axs,dfs)) = - thy |> Sign.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Sign.parent_path; + fun add_one (dnam, axs, dfs) = + Sign.add_path dnam + #> add_defs_infer dfs + #> add_axioms_infer axs + #> Sign.parent_path; - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); + val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy'; in thy |> Sign.add_path comp_dnam |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) diff -r db230399f890 -r 65232054ffd0 src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Tue Oct 27 22:56:14 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/Tools/cont_consts.ML - ID: $Id$ Author: Tobias Mayr, David von Oheimb, and Markus Wenzel HOLCF version of consts: handle continuous function types in mixfix @@ -12,7 +11,7 @@ val add_consts_i: (binding * typ * mixfix) list -> theory -> theory end; -structure ContConsts :> CONT_CONSTS = +structure ContConsts: CONT_CONSTS = struct @@ -29,18 +28,23 @@ | change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) | change_arrow _ _ = sys_error "cont_consts: change_arrow"; -fun trans_rules name2 name1 n mx = let - fun argnames _ 0 = [] - | argnames c n = chr c::argnames (c+1) (n-1); - val vnames = argnames (ord "A") n; - val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); - in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), - Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") - [t,Variable arg])) - (Constant name1,vnames))] - @(case mx of InfixName _ => [extra_parse_rule] - | InfixlName _ => [extra_parse_rule] - | InfixrName _ => [extra_parse_rule] | _ => []) end; +fun trans_rules name2 name1 n mx = + let + fun argnames _ 0 = [] + | argnames c n = chr c::argnames (c+1) (n-1); + val vnames = argnames (ord "A") n; + val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); + in + [Syntax.ParsePrintRule + (Syntax.mk_appl (Constant name2) (map Variable vnames), + fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg]) + vnames (Constant name1))] @ + (case mx of + InfixName _ => [extra_parse_rule] + | InfixlName _ => [extra_parse_rule] + | InfixrName _ => [extra_parse_rule] + | _ => []) + end; (* transforming infix/mixfix declarations of constants with type ...->... @@ -59,7 +63,8 @@ (const_binding mx syn, T, InfixrName (Binding.name_of syn, p)) | fix_mixfix decl = decl; -fun transform decl = let +fun transform decl = + let val (c, T, mx) = fix_mixfix decl; val c1 = Binding.name_of c; val c2 = "_cont_" ^ c1; diff -r db230399f890 -r 65232054ffd0 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 27 22:56:14 2009 +0100 @@ -702,12 +702,11 @@ result end; -fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) : - (bool * term) list = +fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) = union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); fun discr (initems : (LA_Data.decomp * int) list) : bool list = - map fst (Library.foldl add_datoms ([],initems)); + map fst (fold add_datoms initems []); fun refutes ctxt params show_ex : (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option = diff -r db230399f890 -r 65232054ffd0 src/Provers/order.ML --- a/src/Provers/order.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Provers/order.ML Tue Oct 27 22:56:14 2009 +0100 @@ -697,9 +697,9 @@ dfs_visit along with u form a connected component. We collect all the connected components together in a list, which is what is returned. *) - Library.foldl (fn (comps,u) => + fold (fn u => fn comps => if been_visited u then comps - else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) ([],(!finish)) + else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) [] end; diff -r db230399f890 -r 65232054ffd0 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Provers/splitter.ML Tue Oct 27 22:56:14 2009 +0100 @@ -151,7 +151,7 @@ (* add all loose bound variables in t to list is *) -fun add_lbnos (is,t) = add_loose_bnos (t,0,is); +fun add_lbnos t is = add_loose_bnos (t, 0, is); (* check if the innermost abstraction that needs to be removed has a body of type T; otherwise the expansion thm will fail later on @@ -191,7 +191,7 @@ fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) = if n > length ts then [] else let val lev = length apsns - val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts)) + val lbnos = fold add_lbnos (Library.take (n, ts)) [] val flbnos = List.filter (fn i => i < lev) lbnos val tt = incr_boundvars (~lev) t in if null flbnos then @@ -253,20 +253,21 @@ | posns Ts pos apsns t = let val (h, ts) = strip_comb t - fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a); - val a = case h of - Const(c, cT) => - let fun find [] = [] - | find ((gcT, pat, thm, T, n)::tups) = - let val t2 = list_comb (h, Library.take (n, ts)) - in if Sign.typ_instance sg (cT, gcT) - andalso fomatch sg (Ts,pat,t2) - then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) - else find tups - end - in find (these (AList.lookup (op =) cmap c)) end - | _ => [] - in snd(Library.foldl iter ((0, a), ts)) end + fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a); + val a = + case h of + Const(c, cT) => + let fun find [] = [] + | find ((gcT, pat, thm, T, n)::tups) = + let val t2 = list_comb (h, Library.take (n, ts)) + in if Sign.typ_instance sg (cT, gcT) + andalso fomatch sg (Ts,pat,t2) + then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) + else find tups + end + in find (these (AList.lookup (op =) cmap c)) end + | _ => [] + in snd (fold iter ts (0, a)) end in posns Ts [] [] t end; fun nth_subgoal i thm = List.nth (prems_of thm, i-1); @@ -336,8 +337,8 @@ (Logic.strip_assums_concl (Thm.prop_of thm')))); val cert = cterm_of (Thm.theory_of_thm state); val cntxt = mk_cntxt_splitthm t tt TB; - val abss = Library.foldl (fn (t, T) => Abs ("", T, t)); - in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm' + val abss = fold (fn T => fn t => Abs ("", T, t)); + in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm' end; diff -r db230399f890 -r 65232054ffd0 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Oct 27 22:56:14 2009 +0100 @@ -716,8 +716,9 @@ quote name ^ " has no computational content") in (Reconstruct.reconstruct_proof thy prop prf, vs) end; - val defs = Library.foldl (fn (defs, (prf, vs)) => - fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms); + val defs = + fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf)) + (map prep_thm thms) []; fun add_def (s, (vs, ((t, u), (prf, _)))) thy = (case Sign.const_type thy (extr_name s vs) of diff -r db230399f890 -r 65232054ffd0 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Pure/Proof/reconstruct.ML Tue Oct 27 22:56:14 2009 +0100 @@ -40,11 +40,11 @@ fun mk_var env Ts T = let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) - in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end; + in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; -fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) = - (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, - TVar (("'t", maxidx + 1), s)); +fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = + (TVar (("'t", maxidx + 1), S), + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); val mk_abs = fold (fn T => fn u => Abs ("", T, u)); @@ -73,14 +73,14 @@ | infer_type thy env Ts vTs (t as Free (s, T)) = if T = dummyT then (case Symtab.lookup vTs s of NONE => - let val (env', T) = mk_tvar (env, []) + let val (T, env') = mk_tvar [] env in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error" | infer_type thy env Ts vTs (Abs (s, T, t)) = let - val (env', T') = if T = dummyT then mk_tvar (env, []) else (env, T); + val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t in (Abs (s, T', t'), T' --> U, vTs', env'') end | infer_type thy env Ts vTs (t $ u) = @@ -90,7 +90,7 @@ in (case chaseT env2 T of Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') | _ => - let val (env3, V) = mk_tvar (env2, []) + let val (V, env3) = mk_tvar [] env2 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) end | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) @@ -99,21 +99,24 @@ fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); -fun decompose thy Ts (env, p as (t, u)) = - let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p - else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us)) - in case pairself (strip_comb o Envir.head_norm env) p of +fun decompose thy Ts (p as (t, u)) env = + let + fun rigrig (a, T) (b, U) uT ts us = + if a <> b then cantunify thy p + else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) + in + case pairself (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us | ((Bound i, ts), (Bound j, us)) => rigrig (i, dummyT) (j, dummyT) (K o K) ts us | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => - decompose thy (T::Ts) (unifyT thy env T U, (t, u)) + decompose thy (T::Ts) (t, u) (unifyT thy env T U) | ((Abs (_, T, t), []), _) => - decompose thy (T::Ts) (env, (t, incr_boundvars 1 u $ Bound 0)) + decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env | (_, (Abs (_, T, u), [])) => - decompose thy (T::Ts) (env, (incr_boundvars 1 t $ Bound 0, u)) - | _ => (env, [(mk_abs Ts t, mk_abs Ts u)]) + decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env + | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) end; fun make_constraints_cprf thy env cprf = @@ -125,7 +128,7 @@ in (prop, prf, cs, Pattern.unify thy (t', u') env, vTs) handle Pattern.Pattern => - let val (env', cs') = decompose thy [] (env, (t', u')) + let val (cs', env') = decompose thy [] (t', u') env in (prop, prf, cs @ cs', env', vTs) end | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u') @@ -135,10 +138,10 @@ let val tvars = OldTerm.term_tvars prop; val tfrees = OldTerm.term_tfrees prop; - val (env', Ts) = + val (Ts, env') = (case opTs of - NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) - | SOME Ts => (env, Ts)); + NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env + | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) (forall_intr_vfs prop) handle Library.UnequalLengths => error ("Wrong number of type arguments for " ^ @@ -152,8 +155,10 @@ handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = let - val (env', T) = (case opT of - NONE => mk_tvar (env, []) | SOME T => (env, T)); + val (T, env') = + (case opT of + NONE => mk_tvar [] env + | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), @@ -167,7 +172,7 @@ end | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = let - val (env', t) = mk_var env Ts propT; + val (t, env') = mk_var env Ts propT; val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') end @@ -178,7 +183,7 @@ add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) env'' vTs'' (u, u') | (t, prf1, cnstrts', env'', vTs'') => - let val (env''', v) = mk_var env'' Ts propT + let val (v, env''') = mk_var env'' Ts propT in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) env''' vTs'' (t, Logic.mk_implies (u, v)) end) @@ -192,7 +197,7 @@ in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end | (u, prf, cnstrts, env2, vTs2) => - let val (env3, v) = mk_var env2 Ts (U --> propT); + let val (v, env3) = mk_var env2 Ts (U --> propT); in add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 (u, Const ("all", (U --> propT) --> propT) $ v) @@ -202,14 +207,14 @@ (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env', vTs') => - let val (env'', t) = mk_var env' Ts T + let val (t, env'') = mk_var env' Ts T in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') end | (u, prf, cnstrts, env', vTs') => let - val (env1, T) = mk_tvar (env', []); - val (env2, v) = mk_var env1 Ts (T --> propT); - val (env3, t) = mk_var env2 Ts T + val (T, env1) = mk_tvar [] env'; + val (v, env2) = mk_var env1 Ts (T --> propT); + val (t, env3) = mk_var env2 Ts T in add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' (u, Const ("all", (T --> propT) --> propT) $ v) @@ -267,7 +272,7 @@ (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif => cantunify thy (tn1, tn2) else - let val (env', cs') = decompose thy [] (env, (tn1, tn2)) + let val (cs', env') = decompose thy [] (tn1, tn2) env in if cs' = [(tn1, tn2)] then apsnd (cons (false, (tn1, tn2), vs)) (search env ps) else search env' (map (fn q => (true, q, vs)) cs' @ ps) diff -r db230399f890 -r 65232054ffd0 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Oct 27 22:55:27 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Tue Oct 27 22:56:14 2009 +0100 @@ -1139,8 +1139,8 @@ end and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = - transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1 - (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems')) + transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 + (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) (if changed > 0 then mut_impc (rev prems') concl (rev rrss') (rev asms') [] [] [] [] ss ~1 changed