src/HOL/Tools/inductive_codegen.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15660 255055554c67
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -49,12 +49,12 @@
     1.4    in (case concl_of thm of
     1.5        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
     1.6          Const (s, _) =>
     1.7 -          let val cs = Library.foldr add_term_consts (prems_of thm, [])
     1.8 +          let val cs = foldr add_term_consts [] (prems_of thm)
     1.9            in (CodegenData.put
    1.10              {intros = Symtab.update ((s,
    1.11                 getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
    1.12 -             graph = Library.foldr (uncurry (Graph.add_edge o pair s))
    1.13 -               (cs, Library.foldl add_node (graph, s :: cs)),
    1.14 +             graph = foldr (uncurry (Graph.add_edge o pair s))
    1.15 +               (Library.foldl add_node (graph, s :: cs)) cs,
    1.16               eqns = eqns} thy, thm)
    1.17            end
    1.18        | _ => (warn thm; p))
    1.19 @@ -190,7 +190,7 @@
    1.20  fun cprod ([], ys) = []
    1.21    | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
    1.22  
    1.23 -fun cprods xss = Library.foldr (map op :: o cprod) (xss, [[]]);
    1.24 +fun cprods xss = foldr (map op :: o cprod) [[]] xss;
    1.25  
    1.26  datatype mode = Mode of (int list option list * int list) * mode option list;
    1.27  
    1.28 @@ -526,7 +526,7 @@
    1.29          NONE => gr
    1.30        | SOME (names, intrs) =>
    1.31            mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
    1.32 -            (gr, Library.foldr add_term_consts (ts, []))
    1.33 +            (gr, foldr add_term_consts [] ts)
    1.34  
    1.35  and mk_ind_def thy gr dep names modecs factorcs intrs =
    1.36    let val ids = map (mk_const_id (sign_of thy)) names