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