--- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:58 2009 +0200
@@ -221,7 +221,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname::tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a datatype")
@@ -230,7 +230,7 @@
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
-fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
+fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
let
fun constrs_of (_, (_, _, cs)) =
map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;