src/HOL/Tools/inductive_codegen.ML

             | xs => snd (snd (snd (split_last xs)))))
         in CodegenData.put
           {intros = intros |>
            Symtab.update (s, (AList.update Thm.eq_thm_prop
              (thm, (thyname_of s, nparms)) rules)),
-           graph = foldr (uncurry (Graph.add_edge o pair s))
+           graph = List.foldr (uncurry (Graph.add_edge o pair s))
              (Library.foldl add_node (graph, s :: cs)) cs,
            eqns = eqns} thy
         end
     | _ => (warn thm; thy))
   end) I);

      else [[]];
 
 fun cprod ([], ys) = []
   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
 
-fun cprods xss = foldr (map op :: o cprod) [[]] xss;
+fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
 
 datatype mode = Mode of (int list option list * int list) * int list * mode option list;
 
 fun modes_of modes t =
   let

       apfst (Pretty.block o cons (str (s ^ " = ")) o single)
         (invoke_codegen thy defs dep module false t gr);
 
     val (in_ts, out_ts) = get_args is 1 ts;
     val ((all_vs', eqs), in_ts') =
-      foldl_map check_constrt ((all_vs, []), in_ts);
+      Library.foldl_map check_constrt ((all_vs, []), in_ts);
 
     fun compile_prems out_ts' vs names [] gr =
           let
             val (out_ps, gr2) = fold_map
               (invoke_codegen thy defs dep module false) out_ts gr;
             val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
             val ((names', eqs'), out_ts'') =
-              foldl_map check_constrt ((names, []), out_ts');
-            val (nvs, out_ts''') = foldl_map distinct_v
+              Library.foldl_map check_constrt ((names, []), out_ts');
+            val (nvs, out_ts''') = Library.foldl_map distinct_v
               ((names', map (fn x => (x, [x])) vs), out_ts'');
             val (out_ps', gr4) = fold_map
               (invoke_codegen thy defs dep module false) (out_ts''') gr3;
             val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
           in

             val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
             val SOME (p, mode as SOME (Mode (_, js, _))) =
               select_mode_prem thy modes' vs' ps;
             val ps' = filter_out (equal p) ps;
             val ((names', eqs), out_ts') =
-              foldl_map check_constrt ((names, []), out_ts);
-            val (nvs, out_ts'') = foldl_map distinct_v
+              Library.foldl_map check_constrt ((names, []), out_ts);
+            val (nvs, out_ts'') = Library.foldl_map distinct_v
               ((names', map (fn x => (x, [x])) vs), out_ts');
             val (out_ps, gr0) = fold_map
               (invoke_codegen thy defs dep module false) out_ts'' gr;
             val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
           in