src/HOL/Tools/old_primrec.ML
changeset 33963 977b94b64905
parent 33957 e9afca2118d4
child 33968 f94fb13ecbb3
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Nov 27 08:41:08 2009 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Fri Nov 27 08:41:10 2009 +0100
     1.3 @@ -246,7 +246,7 @@
     1.4  fun gen_primrec_i note def alt_name eqns_atts thy =
     1.5    let
     1.6      val (eqns, atts) = split_list eqns_atts;
     1.7 -    val dt_info = Datatype.get_all thy;
     1.8 +    val dt_info = Datatype_Data.get_all thy;
     1.9      val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
    1.10      val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
    1.11      val dts = find_dts dt_info tnames tnames;