proper handling of type variabl names
authorhaftmann
Wed, 27 Aug 2008 11:24:34 +0200
changeset 2801511635f41abc1
parent 28014 fe36718702aa
child 28016 b46f48256dab
proper handling of type variabl names
src/Pure/Isar/code_unit.ML
     1.1 --- a/src/Pure/Isar/code_unit.ML	Wed Aug 27 11:24:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Wed Aug 27 11:24:34 2008 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4          val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
     1.5          val (tyco, _) = last_typ (c, ty) ty_decl;
     1.6          val (_, vs) = last_typ (c, ty) ty;
     1.7 -      in ((tyco, map snd vs), (c, (map fst vs, ty_decl))) end;
     1.8 +      in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
     1.9      fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
    1.10        let
    1.11          val _ = if tyco' <> tyco