eliminated some old folds;
authorwenzelm
Tue Oct 27 22:56:14 2009 +0100 (2009-10-27)
changeset 3324565232054ffd0
parent 33244 db230399f890
child 33246 46e47aa1558f
eliminated some old folds;
src/FOLP/simp.ML
src/HOL/Import/shuffler.ML
src/HOL/Matrix/cplex/CplexMatrixConverter.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/meson.ML
src/HOLCF/IOA/ABP/Check.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/cont_consts.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/order.ML
src/Provers/splitter.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Oct 27 22:55:27 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Oct 27 22:56:14 2009 +0100
     1.3 @@ -254,13 +254,13 @@
     1.4  
     1.5  val insert_thms = fold_rev insert_thm_warn;
     1.6  
     1.7 -fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
     1.8 +fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
     1.9  let val thms = mk_simps thm
    1.10  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.11        simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
    1.12  end;
    1.13  
    1.14 -val op addrews = Library.foldl addrew;
    1.15 +fun ss addrews thms = fold addrew thms ss;
    1.16  
    1.17  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.18  let val congs' = thms @ congs;
    1.19 @@ -287,7 +287,7 @@
    1.20        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.21  end;
    1.22  
    1.23 -fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.24 +fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
    1.25  let fun find((p as (th,ths))::ps',ps) =
    1.26            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.27        | find([],simps') =
    1.28 @@ -298,7 +298,7 @@
    1.29        simps = simps', simp_net = delete_thms thms simp_net }
    1.30  end;
    1.31  
    1.32 -val op delrews = Library.foldl delrew;
    1.33 +fun ss delrews thms = fold delrew thms ss;
    1.34  
    1.35  
    1.36  fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) =
     2.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 27 22:55:27 2009 +0100
     2.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 27 22:56:14 2009 +0100
     2.3 @@ -248,16 +248,16 @@
     2.4          val tvars = OldTerm.term_tvars t
     2.5          val tfree_names = OldTerm.add_term_tfree_names(t,[])
     2.6          val (type_inst,_) =
     2.7 -            Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
     2.8 +            fold (fn (w as (v,_), S) => fn (inst, used) =>
     2.9                        let
    2.10                            val v' = Name.variant used v
    2.11                        in
    2.12                            ((w,TFree(v',S))::inst,v'::used)
    2.13                        end)
    2.14 -                  (([],tfree_names),tvars)
    2.15 +                  tvars ([], tfree_names)
    2.16          val t' = subst_TVars type_inst t
    2.17      in
    2.18 -        (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
    2.19 +        (t', map (fn (w,TFree(v,S)) => (v,TVar(w,S))
    2.20                    | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
    2.21      end
    2.22  
     3.1 --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Tue Oct 27 22:55:27 2009 +0100
     3.2 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Tue Oct 27 22:56:14 2009 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4              set_elem vec (s2i v) (if positive then num else "-"^num)
     3.5            | setprod _ _ _ = raise (Converter "term is not a normed product")        
     3.6  
     3.7 -        fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts)
     3.8 +        fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector
     3.9            | sum2vec t = setprod empty_vector true t                                                
    3.10  
    3.11          fun constrs2Ab j A b [] = (A, b)
    3.12 @@ -100,9 +100,9 @@
    3.13  
    3.14  fun convert_results (cplex.Optimal (opt, entries)) name2index =
    3.15      let
    3.16 -        fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value) 
    3.17 +        fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value
    3.18      in
    3.19 -        (opt, Library.foldl setv (matrix_builder.empty_vector, entries))
    3.20 +        (opt, fold setv entries (matrix_builder.empty_vector))
    3.21      end
    3.22    | convert_results _ _ = raise (Converter "No optimal result")
    3.23  
     4.1 --- a/src/HOL/Tools/TFL/post.ML	Tue Oct 27 22:55:27 2009 +0100
     4.2 +++ b/src/HOL/Tools/TFL/post.ML	Tue Oct 27 22:56:14 2009 +0100
     4.3 @@ -189,12 +189,11 @@
     4.4  in
     4.5  fun derive_init_eqs sgn rules eqs = 
     4.6      let 
     4.7 -      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
     4.8 -                      eqs
     4.9 -      fun countlist l = 
    4.10 -          (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
    4.11 +      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) eqs
    4.12 +      fun countlist l =
    4.13 +        rev (snd (fold (fn e => fn (i, L) => (i + 1, (e, i) :: L)) l (0, [])))
    4.14      in
    4.15 -      maps (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths)
    4.16 +      maps (fn (e, i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths)
    4.17      end;
    4.18  end;
    4.19  
     5.1 --- a/src/HOL/Tools/choice_specification.ML	Tue Oct 27 22:55:27 2009 +0100
     5.2 +++ b/src/HOL/Tools/choice_specification.ML	Tue Oct 27 22:56:14 2009 +0100
     5.3 @@ -165,7 +165,7 @@
     5.4          val cnames = map (fst o dest_Const) proc_consts
     5.5          fun post_process (arg as (thy,thm)) =
     5.6              let
     5.7 -                fun inst_all thy (thm,v) =
     5.8 +                fun inst_all thy v thm =
     5.9                      let
    5.10                          val cv = cterm_of thy v
    5.11                          val cT = ctyp_of_term cv
    5.12 @@ -174,7 +174,7 @@
    5.13                          thm RS spec'
    5.14                      end
    5.15                  fun remove_alls frees thm =
    5.16 -                    Library.foldl (inst_all (Thm.theory_of_thm thm)) (thm,frees)
    5.17 +                    fold (inst_all (Thm.theory_of_thm thm)) frees thm
    5.18                  fun process_single ((name,atts),rew_imp,frees) args =
    5.19                      let
    5.20                          fun undo_imps thm =
     6.1 --- a/src/HOL/Tools/hologic.ML	Tue Oct 27 22:55:27 2009 +0100
     6.2 +++ b/src/HOL/Tools/hologic.ML	Tue Oct 27 22:56:14 2009 +0100
     6.3 @@ -638,8 +638,8 @@
     6.4      val Ts = map snd vs;
     6.5      val t = Const (c, Ts ---> T);
     6.6      val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
     6.7 -    fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
     6.8 -  in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
     6.9 +    fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T);
    6.10 +  in fold app (mk_fTs Ts T ~~ vs) tt end;
    6.11  
    6.12  
    6.13  (* open state monads *)
     7.1 --- a/src/HOL/Tools/meson.ML	Tue Oct 27 22:55:27 2009 +0100
     7.2 +++ b/src/HOL/Tools/meson.ML	Tue Oct 27 22:56:14 2009 +0100
     7.3 @@ -462,14 +462,13 @@
     7.4  (** Detecting repeated assumptions in a subgoal **)
     7.5  
     7.6  (*The stringtree detects repeated assumptions.*)
     7.7 -fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
     7.8 +fun ins_term t net = Net.insert_term (op aconv) (t, t) net;
     7.9  
    7.10  (*detects repetitions in a list of terms*)
    7.11  fun has_reps [] = false
    7.12    | has_reps [_] = false
    7.13    | has_reps [t,u] = (t aconv u)
    7.14 -  | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
    7.15 -                  handle Net.INSERT => true;
    7.16 +  | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true;
    7.17  
    7.18  (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
    7.19  fun TRYING_eq_assume_tac 0 st = Seq.single st
     8.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Tue Oct 27 22:55:27 2009 +0100
     8.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Tue Oct 27 22:56:14 2009 +0100
     8.3 @@ -15,8 +15,8 @@
     8.4  fun check(extacts,intacts,string_of_a,startsI,string_of_s,
     8.5            nexts,hom,transA,startsS) =
     8.6    let fun check_s(s,unchecked,checked) =
     8.7 -        let fun check_sa(unchecked,a) =
     8.8 -              let fun check_sas(unchecked,t) =
     8.9 +        let fun check_sa a unchecked =
    8.10 +              let fun check_sas t unchecked =
    8.11                      (if a mem extacts then
    8.12                            (if transA(hom s,a,hom t) then ( )
    8.13                             else (writeln("Error: Mapping of Externals!");
    8.14 @@ -29,8 +29,8 @@
    8.15                                   string_of_a a; writeln"";
    8.16                                   string_of_s t;writeln"";writeln"" ));
    8.17                       if t mem checked then unchecked else insert (op =) t unchecked)
    8.18 -              in Library.foldl check_sas (unchecked,nexts s a) end;
    8.19 -              val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts)
    8.20 +              in fold check_sas (nexts s a) unchecked end;
    8.21 +              val unchecked' = fold check_sa (extacts @ intacts) unchecked
    8.22          in    (if s mem startsI then 
    8.23                      (if hom(s) mem startsS then ()
    8.24                       else writeln("Error: At start states!"))
     9.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Oct 27 22:55:27 2009 +0100
     9.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Oct 27 22:56:14 2009 +0100
     9.3 @@ -17,7 +17,7 @@
     9.4  end;
     9.5  
     9.6  
     9.7 -structure Domain_Axioms :> DOMAIN_AXIOMS =
     9.8 +structure Domain_Axioms : DOMAIN_AXIOMS =
     9.9  struct
    9.10  
    9.11  open Domain_Library;
    9.12 @@ -218,13 +218,13 @@
    9.13            ("bisim_def",
    9.14             %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
    9.15            
    9.16 -      fun add_one (thy,(dnam,axs,dfs)) =
    9.17 -          thy |> Sign.add_path dnam
    9.18 -              |> add_defs_infer dfs
    9.19 -              |> add_axioms_infer axs
    9.20 -              |> Sign.parent_path;
    9.21 +      fun add_one (dnam, axs, dfs) =
    9.22 +          Sign.add_path dnam
    9.23 +          #> add_defs_infer dfs
    9.24 +          #> add_axioms_infer axs
    9.25 +          #> Sign.parent_path;
    9.26  
    9.27 -      val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
    9.28 +      val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy';
    9.29  
    9.30      in thy |> Sign.add_path comp_dnam  
    9.31             |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
    10.1 --- a/src/HOLCF/Tools/cont_consts.ML	Tue Oct 27 22:55:27 2009 +0100
    10.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Tue Oct 27 22:56:14 2009 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOLCF/Tools/cont_consts.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
    10.7  
    10.8  HOLCF version of consts: handle continuous function types in mixfix
    10.9 @@ -12,7 +11,7 @@
   10.10    val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
   10.11  end;
   10.12  
   10.13 -structure ContConsts :> CONT_CONSTS =
   10.14 +structure ContConsts: CONT_CONSTS =
   10.15  struct
   10.16  
   10.17  
   10.18 @@ -29,18 +28,23 @@
   10.19  |   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
   10.20  |   change_arrow _ _               = sys_error "cont_consts: change_arrow";
   10.21  
   10.22 -fun trans_rules name2 name1 n mx = let
   10.23 -  fun argnames _ 0 = []
   10.24 -  |   argnames c n = chr c::argnames (c+1) (n-1);
   10.25 -  val vnames = argnames (ord "A") n;
   10.26 -  val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
   10.27 -  in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames),
   10.28 -                          Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
   10.29 -                                                [t,Variable arg]))
   10.30 -                          (Constant name1,vnames))]
   10.31 -     @(case mx of InfixName _ => [extra_parse_rule]
   10.32 -                | InfixlName _ => [extra_parse_rule]
   10.33 -                | InfixrName _ => [extra_parse_rule] | _ => []) end;
   10.34 +fun trans_rules name2 name1 n mx =
   10.35 +  let
   10.36 +    fun argnames _ 0 = []
   10.37 +    |   argnames c n = chr c::argnames (c+1) (n-1);
   10.38 +    val vnames = argnames (ord "A") n;
   10.39 +    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
   10.40 +  in
   10.41 +    [Syntax.ParsePrintRule
   10.42 +      (Syntax.mk_appl (Constant name2) (map Variable vnames),
   10.43 +        fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg])
   10.44 +          vnames (Constant name1))] @
   10.45 +    (case mx of
   10.46 +      InfixName _ => [extra_parse_rule]
   10.47 +    | InfixlName _ => [extra_parse_rule]
   10.48 +    | InfixrName _ => [extra_parse_rule]
   10.49 +    | _ => [])
   10.50 +  end;
   10.51  
   10.52  
   10.53  (* transforming infix/mixfix declarations of constants with type ...->...
   10.54 @@ -59,7 +63,8 @@
   10.55                 (const_binding mx syn, T,       InfixrName (Binding.name_of syn, p))
   10.56    | fix_mixfix decl = decl;
   10.57  
   10.58 -fun transform decl = let
   10.59 +fun transform decl =
   10.60 +    let
   10.61          val (c, T, mx) = fix_mixfix decl;
   10.62          val c1 = Binding.name_of c;
   10.63          val c2 = "_cont_" ^ c1;
    11.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 27 22:55:27 2009 +0100
    11.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 27 22:56:14 2009 +0100
    11.3 @@ -702,12 +702,11 @@
    11.4    result
    11.5  end;
    11.6  
    11.7 -fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) :
    11.8 -  (bool * term) list =
    11.9 +fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) =
   11.10    union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
   11.11  
   11.12  fun discr (initems : (LA_Data.decomp * int) list) : bool list =
   11.13 -  map fst (Library.foldl add_datoms ([],initems));
   11.14 +  map fst (fold add_datoms initems []);
   11.15  
   11.16  fun refutes ctxt params show_ex :
   11.17      (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option =
    12.1 --- a/src/Provers/order.ML	Tue Oct 27 22:55:27 2009 +0100
    12.2 +++ b/src/Provers/order.ML	Tue Oct 27 22:56:14 2009 +0100
    12.3 @@ -697,9 +697,9 @@
    12.4       dfs_visit along with u form a connected component. We
    12.5       collect all the connected components together in a
    12.6       list, which is what is returned. *)
    12.7 -  Library.foldl (fn (comps,u) =>
    12.8 +  fold (fn u => fn comps =>
    12.9        if been_visited u then comps
   12.10 -      else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  ([],(!finish))
   12.11 +      else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) []
   12.12  end;
   12.13  
   12.14  
    13.1 --- a/src/Provers/splitter.ML	Tue Oct 27 22:55:27 2009 +0100
    13.2 +++ b/src/Provers/splitter.ML	Tue Oct 27 22:56:14 2009 +0100
    13.3 @@ -151,7 +151,7 @@
    13.4  
    13.5  
    13.6  (* add all loose bound variables in t to list is *)
    13.7 -fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
    13.8 +fun add_lbnos t is = add_loose_bnos (t, 0, is);
    13.9  
   13.10  (* check if the innermost abstraction that needs to be removed
   13.11     has a body of type T; otherwise the expansion thm will fail later on
   13.12 @@ -191,7 +191,7 @@
   13.13  fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
   13.14    if n > length ts then []
   13.15    else let val lev = length apsns
   13.16 -           val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
   13.17 +           val lbnos = fold add_lbnos (Library.take (n, ts)) []
   13.18             val flbnos = List.filter (fn i => i < lev) lbnos
   13.19             val tt = incr_boundvars (~lev) t
   13.20         in if null flbnos then
   13.21 @@ -253,20 +253,21 @@
   13.22        | posns Ts pos apsns t =
   13.23            let
   13.24              val (h, ts) = strip_comb t
   13.25 -            fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
   13.26 -            val a = case h of
   13.27 -              Const(c, cT) =>
   13.28 -                let fun find [] = []
   13.29 -                      | find ((gcT, pat, thm, T, n)::tups) =
   13.30 -                          let val t2 = list_comb (h, Library.take (n, ts))
   13.31 -                          in if Sign.typ_instance sg (cT, gcT)
   13.32 -                                andalso fomatch sg (Ts,pat,t2)
   13.33 -                             then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
   13.34 -                             else find tups
   13.35 -                          end
   13.36 -                in find (these (AList.lookup (op =) cmap c)) end
   13.37 -            | _ => []
   13.38 -          in snd(Library.foldl iter ((0, a), ts)) end
   13.39 +            fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a);
   13.40 +            val a =
   13.41 +              case h of
   13.42 +                Const(c, cT) =>
   13.43 +                  let fun find [] = []
   13.44 +                        | find ((gcT, pat, thm, T, n)::tups) =
   13.45 +                            let val t2 = list_comb (h, Library.take (n, ts))
   13.46 +                            in if Sign.typ_instance sg (cT, gcT)
   13.47 +                                  andalso fomatch sg (Ts,pat,t2)
   13.48 +                               then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
   13.49 +                               else find tups
   13.50 +                            end
   13.51 +                  in find (these (AList.lookup (op =) cmap c)) end
   13.52 +              | _ => []
   13.53 +          in snd (fold iter ts (0, a)) end
   13.54    in posns Ts [] [] t end;
   13.55  
   13.56  fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
   13.57 @@ -336,8 +337,8 @@
   13.58        (Logic.strip_assums_concl (Thm.prop_of thm'))));
   13.59      val cert = cterm_of (Thm.theory_of_thm state);
   13.60      val cntxt = mk_cntxt_splitthm t tt TB;
   13.61 -    val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
   13.62 -  in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm'
   13.63 +    val abss = fold (fn T => fn t => Abs ("", T, t));
   13.64 +  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
   13.65    end;
   13.66  
   13.67  
    14.1 --- a/src/Pure/Proof/extraction.ML	Tue Oct 27 22:55:27 2009 +0100
    14.2 +++ b/src/Pure/Proof/extraction.ML	Tue Oct 27 22:56:14 2009 +0100
    14.3 @@ -716,8 +716,9 @@
    14.4            quote name ^ " has no computational content")
    14.5        in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
    14.6  
    14.7 -    val defs = Library.foldl (fn (defs, (prf, vs)) =>
    14.8 -      fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
    14.9 +    val defs =
   14.10 +      fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf))
   14.11 +        (map prep_thm thms) [];
   14.12  
   14.13      fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
   14.14        (case Sign.const_type thy (extr_name s vs) of
    15.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Oct 27 22:55:27 2009 +0100
    15.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Oct 27 22:56:14 2009 +0100
    15.3 @@ -40,11 +40,11 @@
    15.4  
    15.5  fun mk_var env Ts T =
    15.6    let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
    15.7 -  in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
    15.8 +  in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end;
    15.9  
   15.10 -fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
   15.11 -  (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
   15.12 -   TVar (("'t", maxidx + 1), s));
   15.13 +fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) =
   15.14 +  (TVar (("'t", maxidx + 1), S),
   15.15 +    Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv});
   15.16  
   15.17  val mk_abs = fold (fn T => fn u => Abs ("", T, u));
   15.18  
   15.19 @@ -73,14 +73,14 @@
   15.20    | infer_type thy env Ts vTs (t as Free (s, T)) =
   15.21        if T = dummyT then (case Symtab.lookup vTs s of
   15.22            NONE =>
   15.23 -            let val (env', T) = mk_tvar (env, [])
   15.24 +            let val (T, env') = mk_tvar [] env
   15.25              in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end
   15.26          | SOME T => (Free (s, T), T, vTs, env))
   15.27        else (t, T, vTs, env)
   15.28    | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error"
   15.29    | infer_type thy env Ts vTs (Abs (s, T, t)) =
   15.30        let
   15.31 -        val (env', T') = if T = dummyT then mk_tvar (env, []) else (env, T);
   15.32 +        val (T', env') = if T = dummyT then mk_tvar [] env else (T, env);
   15.33          val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t
   15.34        in (Abs (s, T', t'), T' --> U, vTs', env'') end
   15.35    | infer_type thy env Ts vTs (t $ u) =
   15.36 @@ -90,7 +90,7 @@
   15.37        in (case chaseT env2 T of
   15.38            Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
   15.39          | _ =>
   15.40 -          let val (env3, V) = mk_tvar (env2, [])
   15.41 +          let val (V, env3) = mk_tvar [] env2
   15.42            in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
   15.43        end
   15.44    | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
   15.45 @@ -99,21 +99,24 @@
   15.46  fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
   15.47    Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
   15.48  
   15.49 -fun decompose thy Ts (env, p as (t, u)) =
   15.50 -  let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p
   15.51 -    else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us))
   15.52 -  in case pairself (strip_comb o Envir.head_norm env) p of
   15.53 +fun decompose thy Ts (p as (t, u)) env =
   15.54 +  let
   15.55 +    fun rigrig (a, T) (b, U) uT ts us =
   15.56 +      if a <> b then cantunify thy p
   15.57 +      else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
   15.58 +  in
   15.59 +    case pairself (strip_comb o Envir.head_norm env) p of
   15.60        ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
   15.61      | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
   15.62      | ((Bound i, ts), (Bound j, us)) =>
   15.63          rigrig (i, dummyT) (j, dummyT) (K o K) ts us
   15.64      | ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
   15.65 -        decompose thy (T::Ts) (unifyT thy env T U, (t, u))
   15.66 +        decompose thy (T::Ts) (t, u) (unifyT thy env T U)
   15.67      | ((Abs (_, T, t), []), _) =>
   15.68 -        decompose thy (T::Ts) (env, (t, incr_boundvars 1 u $ Bound 0))
   15.69 +        decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
   15.70      | (_, (Abs (_, T, u), [])) =>
   15.71 -        decompose thy (T::Ts) (env, (incr_boundvars 1 t $ Bound 0, u))
   15.72 -    | _ => (env, [(mk_abs Ts t, mk_abs Ts u)])
   15.73 +        decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
   15.74 +    | _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
   15.75    end;
   15.76  
   15.77  fun make_constraints_cprf thy env cprf =
   15.78 @@ -125,7 +128,7 @@
   15.79        in
   15.80          (prop, prf, cs, Pattern.unify thy (t', u') env, vTs)
   15.81          handle Pattern.Pattern =>
   15.82 -            let val (env', cs') = decompose thy [] (env, (t', u'))
   15.83 +            let val (cs', env') = decompose thy [] (t', u') env
   15.84              in (prop, prf, cs @ cs', env', vTs) end
   15.85          | Pattern.Unif =>
   15.86              cantunify thy (Envir.norm_term env t', Envir.norm_term env u')
   15.87 @@ -135,10 +138,10 @@
   15.88            let
   15.89              val tvars = OldTerm.term_tvars prop;
   15.90              val tfrees = OldTerm.term_tfrees prop;
   15.91 -            val (env', Ts) =
   15.92 +            val (Ts, env') =
   15.93                (case opTs of
   15.94 -                NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
   15.95 -              | SOME Ts => (env, Ts));
   15.96 +                NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
   15.97 +              | SOME Ts => (Ts, env));
   15.98              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
   15.99                (forall_intr_vfs prop) handle Library.UnequalLengths =>
  15.100                  error ("Wrong number of type arguments for " ^
  15.101 @@ -152,8 +155,10 @@
  15.102            handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
  15.103        | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
  15.104            let
  15.105 -            val (env', T) = (case opT of
  15.106 -              NONE => mk_tvar (env, []) | SOME T => (env, T));
  15.107 +            val (T, env') =
  15.108 +              (case opT of
  15.109 +                NONE => mk_tvar [] env
  15.110 +              | SOME T => (T, env));
  15.111              val (t, prf, cnstrts, env'', vTs') =
  15.112                mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
  15.113            in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
  15.114 @@ -167,7 +172,7 @@
  15.115            end
  15.116        | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) =
  15.117            let
  15.118 -            val (env', t) = mk_var env Ts propT;
  15.119 +            val (t, env') = mk_var env Ts propT;
  15.120              val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf;
  15.121            in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs')
  15.122            end
  15.123 @@ -178,7 +183,7 @@
  15.124                  add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts)
  15.125                    env'' vTs'' (u, u')
  15.126              | (t, prf1, cnstrts', env'', vTs'') =>
  15.127 -                let val (env''', v) = mk_var env'' Ts propT
  15.128 +                let val (v, env''') = mk_var env'' Ts propT
  15.129                  in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts)
  15.130                    env''' vTs'' (t, Logic.mk_implies (u, v))
  15.131                  end)
  15.132 @@ -192,7 +197,7 @@
  15.133                 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
  15.134                 end
  15.135             | (u, prf, cnstrts, env2, vTs2) =>
  15.136 -               let val (env3, v) = mk_var env2 Ts (U --> propT);
  15.137 +               let val (v, env3) = mk_var env2 Ts (U --> propT);
  15.138                 in
  15.139                   add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2
  15.140                     (u, Const ("all", (U --> propT) --> propT) $ v)
  15.141 @@ -202,14 +207,14 @@
  15.142            (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of
  15.143               (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
  15.144                   prf, cnstrts, env', vTs') =>
  15.145 -               let val (env'', t) = mk_var env' Ts T
  15.146 +               let val (t, env'') = mk_var env' Ts T
  15.147                 in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs')
  15.148                 end
  15.149             | (u, prf, cnstrts, env', vTs') =>
  15.150                 let
  15.151 -                 val (env1, T) = mk_tvar (env', []);
  15.152 -                 val (env2, v) = mk_var env1 Ts (T --> propT);
  15.153 -                 val (env3, t) = mk_var env2 Ts T
  15.154 +                 val (T, env1) = mk_tvar [] env';
  15.155 +                 val (v, env2) = mk_var env1 Ts (T --> propT);
  15.156 +                 val (t, env3) = mk_var env2 Ts T
  15.157                 in
  15.158                   add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
  15.159                     (u, Const ("all", (T --> propT) --> propT) $ v)
  15.160 @@ -267,7 +272,7 @@
  15.161                      (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif =>
  15.162                         cantunify thy (tn1, tn2)
  15.163                    else
  15.164 -                    let val (env', cs') = decompose thy [] (env, (tn1, tn2))
  15.165 +                    let val (cs', env') = decompose thy [] (tn1, tn2) env
  15.166                      in if cs' = [(tn1, tn2)] then
  15.167                           apsnd (cons (false, (tn1, tn2), vs)) (search env ps)
  15.168                         else search env' (map (fn q => (true, q, vs)) cs' @ ps)
    16.1 --- a/src/Pure/meta_simplifier.ML	Tue Oct 27 22:55:27 2009 +0100
    16.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 27 22:56:14 2009 +0100
    16.3 @@ -1139,8 +1139,8 @@
    16.4        end
    16.5  
    16.6      and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
    16.7 -        transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
    16.8 -            (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
    16.9 +        transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
   16.10 +            (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
   16.11            (if changed > 0 then
   16.12               mut_impc (rev prems') concl (rev rrss') (rev asms')
   16.13                 [] [] [] [] ss ~1 changed