src/HOL/Import/proof_kernel.ML

                 val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
                 val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
                 val (c,asl) = case terms of
                                   [] => raise ERR "x2p" "Bad oracle description"
                                 | (hd::tl) => (hd,tl)
-                val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
+                val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
             in
                 mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
             end
           | x2p (Elem("pspec",[("i",is)],[prf])) =
             let

                                                             then ty2
                                                             else ty
                       | inst_type ty1 ty2 (ty as Type(name,tys)) =
                         Type(name,map (inst_type ty1 ty2) tys)
                 in
-                    foldr (fn (v,th) =>
+                    List.foldr (fn (v,th) =>
                               let
                                   val cdom = fst (dom_rng (fst (dom_rng cty)))
                                   val vty  = type_of v
                                   val newcty = inst_type cdom vty cty
                                   val cc = cterm_of thy (Const(cname,newcty))

                                   mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
                               end) th vlist'
                 end
               | SOME _ => raise ERR "GEN_ABS" "Bad constant"
               | NONE =>
-                foldr (fn (v,th) => mk_ABS v th thy) th vlist'
+                List.foldr (fn (v,th) => mk_ABS v th thy) th vlist'
         val res = HOLThm(rens_of info',th1)
         val _ = message "RESULT:"
         val _ = if_debug pth res
     in
         (thy,res)

                                val _ = ImportRecorder.add_consts consts
                            in
                                Sign.add_consts_i consts thy'
                            end
 
-            val thy1 = foldr (fn(name,thy)=>
+            val thy1 = List.foldr (fn(name,thy)=>
                                 snd (get_defname thyname name thy)) thy1 names
             fun new_name name = fst (get_defname thyname name thy1)
             val names' = map (fn name => (new_name name,name,false)) names
             val (thy',res) = SpecificationPackage.add_specification NONE
                                  names'

                 in
                     (if defname = newname
                      then quotename name
                      else (quotename newname) ^ ": " ^ (quotename name),thy')
                 end
-            val (new_names,thy') = foldr (fn(name,(names,thy)) =>
+            val (new_names,thy') = List.foldr (fn(name,(names,thy)) =>
                                             let
                                                 val (name',thy') = handle_const (name,thy)
                                             in
                                                 (name'::names,thy')
                                             end) ([],thy') names