--- 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