diff -r 12a89103cae6 -r bbf49d7dfd6f src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/type.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -254,7 +254,7 @@
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
+fun lookup_type (TSig {types, ...}) = Name_Space.lookup types;
 
 fun check_decl context (TSig {types, ...}) (c, pos) =
   Name_Space.check_reports context types (c, [pos]);