src/HOL/Tools/old_primrec.ML
changeset 31737 b3f63611784e
parent 31723 f5cafe803b55
child 31784 bd3486c57ba3
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Sun Jun 21 08:38:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Sun Jun 21 08:38:58 2009 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  
     1.5  (* find datatypes which contain all datatypes in tnames' *)
     1.6  
     1.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
     1.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
     1.9    | find_dts dt_info tnames' (tname::tnames) =
    1.10        (case Symtab.lookup dt_info tname of
    1.11            NONE => primrec_err (quote tname ^ " is not a datatype")
    1.12 @@ -230,7 +230,7 @@
    1.13                (tname, dt)::(find_dts dt_info tnames' tnames)
    1.14              else find_dts dt_info tnames' tnames);
    1.15  
    1.16 -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
    1.17 +fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
    1.18    let
    1.19      fun constrs_of (_, (_, _, cs)) =
    1.20        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;