diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/term_sharing.ML
--- a/src/Pure/term_sharing.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/term_sharing.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -19,10 +19,10 @@
 
 fun init thy =
   let
-    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
+    val {classes = (_, algebra), types, ...} = Type.rep_tsig (Sign.tsig_of thy);
 
     val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
-    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
+    val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
     val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
 
     val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);