--- a/src/HOL/Tools/primrec.ML Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Tue Jun 23 16:27:12 2009 +0200
@@ -220,7 +220,7 @@
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
- val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
+ val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
(index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
val {descr, rec_names, rec_rewrites, ...} =