--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Apr 03 10:51:22 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Apr 03 10:51:24 2014 +0200
@@ -158,7 +158,14 @@
val eq: T * T -> bool = op = o pairself #ctrs;
);
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation;
+fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
+ thy
+ |> Sign.root_path
+ |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
+ |> f ctr_sugar
+ |> Sign.restore_naming thy;
+
+val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
fun register_ctr_sugar key ctr_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}