diff -r 6f19e5eb3a44 -r 3634641f9405 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri Oct 13 18:18:58 2006 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Oct 13 18:23:37 2006 +0200 @@ -76,7 +76,7 @@ fun get_clauses thy s = let val {intros, graph, ...} = CodegenData.get thy in case Symtab.lookup intros s of - NONE => (case InductivePackage.get_inductive thy s of + NONE => (case OldInductivePackage.get_inductive thy s of NONE => NONE | SOME ({names, ...}, {intrs, ...}) => SOME (names, thyname_of_const s thy,