src/HOL/Tools/primrec.ML
changeset 31784 bd3486c57ba3
parent 31737 b3f63611784e
child 31786 a5ad48ae17e5
     1.1 --- a/src/HOL/Tools/primrec.ML	Tue Jun 23 15:32:34 2009 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Tue Jun 23 16:27:12 2009 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
     1.5        orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
     1.6      val tnames = distinct (op =) (map (#1 o snd) eqns);
     1.7 -    val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
     1.8 +    val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames;
     1.9      val main_fns = map (fn (tname, {index, ...}) =>
    1.10        (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
    1.11      val {descr, rec_names, rec_rewrites, ...} =