--- a/src/HOL/Tools/inductive_codegen.ML Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jan 01 14:23:39 2009 +0100
@@ -57,7 +57,7 @@
| _ => (warn thm; thy))
| SOME (Const (s, _), _) =>
let
- val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
+ val cs = fold Term.add_const_names (Thm.prems_of thm) [];
val rules = Symtab.lookup_list intros s;
val nparms = (case optnparms of
SOME k => k
@@ -490,7 +490,7 @@
| SOME (names, thyname, nparms, intrs) =>
mk_ind_def thy defs gr dep names (if_library thyname module)
[] (prep_intrs intrs) nparms))
- (gr, foldr OldTerm.add_term_consts [] ts)
+ (gr, fold Term.add_const_names ts [])
and mk_ind_def thy defs gr dep names module modecs intrs nparms =
add_edge_acyclic (hd names, dep) gr handle