--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Apr 10 17:48:17 2014 +0200
@@ -158,12 +158,13 @@
val eq: T * T -> bool = op = o pairself #ctrs;
);
+(* FIXME naming *)
fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
thy
- |> Sign.root_path
+ (*|> Sign.root_path*)
|> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
- |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
- |> Sign.restore_naming thy;
+ (*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
+ (*|> Sign.restore_naming thy*);
val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;