diff -r 35354009ca25 -r 55ac31bc08a4 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Feb 03 15:44:46 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Mon Feb 03 16:33:54 2014 +0100
@@ -209,7 +209,7 @@
        | SOME const' => (const, const')) consts consts'
     val tycos_map = map2 (fn tyco =>
       fn NONE =>
-          error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
+          error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
             "\nhas a user-defined serialization")
         | SOME tyco' => (tyco, tyco')) tycos tycos';
   in (ml_code, (tycos_map, consts_map)) end;