src/HOL/Tools/datatype_realizer.ML
changeset 20071 8f3e1ddb50e6
parent 19806 f860b7a98445
child 20286 4cf8e86a2d29
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4        (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
     1.5          let
     1.6            val Ts = map (typ_of_dtyp descr sorts) cargs;
     1.7 -          val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
     1.8 +          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
     1.9            val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    1.10            val frees = tnames ~~ Ts;
    1.11  
    1.12 @@ -171,8 +171,7 @@
    1.13      fun make_casedist_prem T (cname, cargs) =
    1.14        let
    1.15          val Ts = map (typ_of_dtyp descr sorts) cargs;
    1.16 -        val frees = variantlist
    1.17 -          (DatatypeProp.make_tnames Ts, ["P", "y"]) ~~ Ts;
    1.18 +        val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
    1.19          val free_ts = map Free frees;
    1.20          val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
    1.21        in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop