diff -r dfc7a46c2900 -r 32e0da92c786 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/Pure/Isar/code.ML	Thu Apr 03 10:51:22 2014 +0200
@@ -1232,8 +1232,15 @@
 structure Datatype_Interpretation =
   Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
+fun with_repaired_path f (tyco, serial) thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier tyco)
+  |> f (tyco, serial)
+  |> Sign.restore_naming thy;
+
 fun datatype_interpretation f = Datatype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
+  (fn (tyco, _) => fn thy => with_repaired_path f (tyco, fst (get_type thy tyco)) thy);
 
 fun add_datatype proto_constrs thy =
   let