src/Pure/Isar/instance.ML
changeset 24848 5dbbd33c3236
parent 24713 8b3b6d09ef40
child 24931 e0a2c154df26
     1.1 --- a/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -30,7 +30,8 @@
     1.4      fun prep_arity' raw_arity names =
     1.5        let
     1.6          val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
     1.7 -        val (vs, names') = Name.variants (replicate (length sorts) "'a") names;
     1.8 +        val vs = Name.invents names Name.aT (length sorts);
     1.9 +        val names' = fold Name.declare vs names;
    1.10        in (((tyco, vs ~~ sorts), sort), names') end;
    1.11      val (arities, _) = fold_map prep_arity' raw_arities Name.context;
    1.12      fun get_param tyco ty_subst (param, (c, ty)) =