src/ZF/Tools/datatype_package.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36954 ef698bd61057
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4              @{const_name nat} :: map (#1 o dest_Const) rec_hds
     1.5          val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
     1.6          val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
     1.7 -          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
     1.8 +          (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
     1.9              | _ => I)) con_ty_lists [];
    1.10      in  u $ Ind_Syntax.union_params (hd rec_tms, cs)  end;
    1.11  
    1.12 @@ -193,7 +193,7 @@
    1.13      | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
    1.14         (case head_of X of
    1.15              Const(a,_) => (*recursive occurrence?*)
    1.16 -                          if a mem_string rec_names
    1.17 +                          if member (op =) rec_names a
    1.18                                then arg :: rec_args prems
    1.19                            else rec_args prems
    1.20            | _ => rec_args prems)