1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -776,7 +776,7 @@
     1.4                  val (c,asl) = case terms of
     1.5                                    [] => raise ERR "x2p" "Bad oracle description"
     1.6                                  | (hd::tl) => (hd,tl)
     1.7 -                val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
     1.8 +                val tg = fold_rev (Tag.merge o Tag.read) ors Tag.empty_tag
     1.9              in
    1.10                  mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
    1.11              end
    1.12 @@ -1160,7 +1160,7 @@
    1.13          | replace_name n' _ = ERR "replace_name"
    1.14        (* map: old or fresh name -> old free,
    1.15           invmap: old free which has fresh name assigned to it -> fresh name *)
    1.16 -      fun dis (v, mapping as (map,invmap)) =
    1.17 +      fun dis v (mapping as (map,invmap)) =
    1.18            let val n = name_of v in
    1.19              case Symtab.lookup map n of
    1.20                NONE => (Symtab.update (n, v) map, invmap)
    1.21 @@ -1179,11 +1179,11 @@
    1.22        else
    1.23          let
    1.24            val (_, invmap) =
    1.25 -              List.foldl dis (Symtab.empty, Termtab.empty) frees
    1.26 -          fun make_subst ((oldfree, newname), (intros, elims)) =
    1.27 +              fold dis frees (Symtab.empty, Termtab.empty)
    1.28 +          fun make_subst (oldfree, newname) (intros, elims) =
    1.29                (cterm_of thy oldfree :: intros,
    1.30                 cterm_of thy (replace_name newname oldfree) :: elims)
    1.31 -          val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
    1.32 +          val (intros, elims) = fold make_subst (Termtab.dest invmap) ([], [])
    1.33          in
    1.34            forall_elim_list elims (forall_intr_list intros thm)
    1.35          end
    1.36 @@ -1837,7 +1837,7 @@
    1.37                        | inst_type ty1 ty2 (ty as Type(name,tys)) =
    1.38                          Type(name,map (inst_type ty1 ty2) tys)
    1.39                  in
    1.40 -                    List.foldr (fn (v,th) =>
    1.41 +                    fold_rev (fn v => fn th =>
    1.42                                let
    1.43                                    val cdom = fst (dom_rng (fst (dom_rng cty)))
    1.44                                    val vty  = type_of v
    1.45 @@ -1845,11 +1845,11 @@
    1.46                                    val cc = cterm_of thy (Const(cname,newcty))
    1.47                                in
    1.48                                    mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
    1.49 -                              end) th vlist'
    1.50 +                              end) vlist' th
    1.51                  end
    1.52                | SOME _ => raise ERR "GEN_ABS" "Bad constant"
    1.53                | NONE =>
    1.54 -                List.foldr (fn (v,th) => mk_ABS v th thy) th vlist'
    1.55 +                fold_rev (fn v => fn th => mk_ABS v th thy) vlist' th
    1.56          val res = HOLThm(rens_of info',th1)
    1.57          val _ = message "RESULT:"
    1.58          val _ = if_debug pth res
    1.59 @@ -2020,8 +2020,8 @@
    1.60                                 Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
    1.61                             end
    1.62  
    1.63 -            val thy1 = List.foldr (fn(name,thy)=>
    1.64 -                                snd (get_defname thyname name thy)) thy1 names
    1.65 +            val thy1 = fold_rev (fn name => fn thy =>
    1.66 +                                snd (get_defname thyname name thy)) names thy1
    1.67              fun new_name name = fst (get_defname thyname name thy1)
    1.68              val names' = map (fn name => (new_name name,name,false)) names
    1.69              val (thy',res) = Choice_Specification.add_specification NONE
    1.70 @@ -2041,12 +2041,12 @@
    1.71                       then quotename name
    1.72                       else (quotename newname) ^ ": " ^ (quotename name),thy')
    1.73                  end
    1.74 -            val (new_names,thy') = List.foldr (fn(name,(names,thy)) =>
    1.75 +            val (new_names,thy') = fold_rev (fn name => fn (names, thy) =>
    1.76                                              let
    1.77                                                  val (name',thy') = handle_const (name,thy)
    1.78                                              in
    1.79                                                  (name'::names,thy')
    1.80 -                                            end) ([],thy') names
    1.81 +                                            end) names ([], thy')
    1.82              val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
    1.83                                    "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
    1.84                                   thy'