# HG changeset patch
# User blanchet
# Date 1398639271 -7200
# Node ID 9b311dbd0f55544cbf834076c57ec335d53f4a6d
# Parent  ba2fa4e997294be5760ff49341d9ef56b762dfd1
restored naming trick

diff -r ba2fa4e99729 -r 9b311dbd0f55 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 28 00:54:31 2014 +0200
@@ -122,13 +122,12 @@
   val eq: T * T -> bool = op = o pairself (map #T);
 );
 
-(* FIXME naming *)
 fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy =
   thy
-  (*|> Sign.root_path*)
-  (*|> Sign.add_path (Long_Name.qualifier s)*)
+  |> Sign.root_path
+  |> Sign.add_path (Long_Name.qualifier s)
   |> f fp_sugars
-  (*|> Sign.restore_naming thy*);
+  |> Sign.restore_naming thy;
 
 fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
 
diff -r ba2fa4e99729 -r 9b311dbd0f55 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 28 00:54:31 2014 +0200
@@ -158,13 +158,12 @@
   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;
 
 fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);