# HG changeset patch
# User kuncar
# Date 1397144897 -7200
# Node ID 2ae16e3d8b6d316edbcb694151e5f254fd6fb9e6
# Parent  f54003750e7d123cf1e32efa36c9f2839f42afc4
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created

diff -r f54003750e7d -r 2ae16e3d8b6d src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:17 2014 +0200
@@ -1315,6 +1315,7 @@
   val eq: T * T -> bool = op = o pairself T_of_bnf;
 );
 
+(* FIXME naming *)
 fun with_repaired_path f bnf thy =
   let
     val qualifiers =
@@ -1324,10 +1325,10 @@
       | (_, qs, _) => qs)
   in
     thy
-    |> Sign.root_path
-    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
+    (*|> Sign.root_path*)
+    (*|> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers*)
     |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
-    |> Sign.restore_naming thy
+    (*|> Sign.restore_naming thy*)
   end;
 
 val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
diff -r f54003750e7d -r 2ae16e3d8b6d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:17 2014 +0200
@@ -193,12 +193,13 @@
   val eq: T * T -> bool = op = o pairself #T;
 );
 
+(* FIXME naming *)
 fun with_repaired_path f (fp_sugar as {T, ...} : fp_sugar) thy =
   thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
+  (*|> Sign.root_path*)
+  (*|> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))*)
   |> (fn thy => f (morph_fp_sugar (Morphism.transfer_morphism thy) fp_sugar) thy)
-  |> Sign.restore_naming thy;
+  (*|> Sign.restore_naming thy*);
 
 val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
 
diff -r f54003750e7d -r 2ae16e3d8b6d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- 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;