diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/Isar/object_logic.ML	Mon Feb 15 17:17:51 2010 +0100
@@ -84,10 +84,9 @@
 
 (* typedecl *)
 
-fun typedecl (a, vs, mx) thy =
+fun typedecl (b, vs, mx) thy =
   let
     val base_sort = get_base_sort thy;
-    val b = Binding.map_name (Syntax.type_name mx) a;
     val _ = has_duplicates (op =) vs andalso
       error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
     val name = Sign.full_name thy b;
@@ -95,7 +94,7 @@
     val T = Type (name, map (fn v => TFree (v, [])) vs);
   in
     thy
-    |> Sign.add_types [(a, n, mx)]
+    |> Sign.add_types [(b, n, mx)]
     |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
     |> pair T
   end;
@@ -106,7 +105,7 @@
 local
 
 fun gen_add_judgment add_consts (b, T, mx) thy =
-  let val c = Sign.full_name thy (Binding.map_name (Syntax.const_name mx) b) in
+  let val c = Sign.full_name thy b in
     thy
     |> add_consts [(b, T, mx)]
     |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')