# HG changeset patch
# User haftmann
# Date 1219829074 -7200
# Node ID 11635f41abc17c659f7f5a2bf01a121d5af76841
# Parent  fe36718702aa78ee88c3042b173d9b9f24562a6c
proper handling of type variabl names

diff -r fe36718702aa -r 11635f41abc1 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Wed Aug 27 11:24:32 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Wed Aug 27 11:24:34 2008 +0200
@@ -307,7 +307,7 @@
         val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
         val (tyco, _) = last_typ (c, ty) ty_decl;
         val (_, vs) = last_typ (c, ty) ty;
-      in ((tyco, map snd vs), (c, (map fst vs, ty_decl))) end;
+      in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
     fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
       let
         val _ = if tyco' <> tyco