diff -r d320f2f9f331 -r fe57d786fd5b src/Pure/term_sharing.ML
--- a/src/Pure/term_sharing.ML	Sun Nov 20 13:29:12 2011 +0100
+++ b/src/Pure/term_sharing.ML	Sun Nov 20 15:21:22 2011 +0100
@@ -21,7 +21,7 @@
   let
     val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
 
-    val sort = perhaps (try (Sorts.certify_sort algebra));
+    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 const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
 
@@ -36,8 +36,8 @@
             val T' =
               (case T of
                 Type (a, Ts) => Type (tycon a, map typ Ts)
-              | TFree (a, S) => TFree (a, sort S)
-              | TVar (a, S) => TVar (a, sort S));
+              | TFree (a, S) => TFree (a, map class S)
+              | TVar (a, S) => TVar (a, map class S));
             val _ = Unsynchronized.change typs (Typtab.update (T', ()));
           in T' end);