--- 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) =
--- 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
--- 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")
--- 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;
--- 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 =
--- 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 *)
--- 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
--- 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!"))
--- 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 []))
--- 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;
--- 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 =
--- 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;
--- 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;
--- 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
--- 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)
--- 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