--- a/src/HOL/Tools/inductive_codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -49,12 +49,12 @@
in (case concl_of thm of
_ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
Const (s, _) =>
- let val cs = Library.foldr add_term_consts (prems_of thm, [])
+ let val cs = foldr add_term_consts [] (prems_of thm)
in (CodegenData.put
{intros = Symtab.update ((s,
getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
- graph = Library.foldr (uncurry (Graph.add_edge o pair s))
- (cs, Library.foldl add_node (graph, s :: cs)),
+ graph = foldr (uncurry (Graph.add_edge o pair s))
+ (Library.foldl add_node (graph, s :: cs)) cs,
eqns = eqns} thy, thm)
end
| _ => (warn thm; p))
@@ -190,7 +190,7 @@
fun cprod ([], ys) = []
| cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
-fun cprods xss = Library.foldr (map op :: o cprod) (xss, [[]]);
+fun cprods xss = foldr (map op :: o cprod) [[]] xss;
datatype mode = Mode of (int list option list * int list) * mode option list;
@@ -526,7 +526,7 @@
NONE => gr
| SOME (names, intrs) =>
mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
- (gr, Library.foldr add_term_consts (ts, []))
+ (gr, foldr add_term_consts [] ts)
and mk_ind_def thy gr dep names modecs factorcs intrs =
let val ids = map (mk_const_id (sign_of thy)) names