diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -431,7 +431,7 @@
       |> fold (ensure_fun thy arities eqngr) cs
       |> fold (ensure_rhs thy arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
-    val pp = Syntax.pp_global thy;
+    val pp = Context.pretty_global thy;
     val algebra = Sorts.subalgebra pp (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);