1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:17 2014 +0200
     1.3 @@ -1315,6 +1315,7 @@
     1.4    val eq: T * T -> bool = op = o pairself T_of_bnf;
     1.5  );
     1.6  
     1.7 +(* FIXME naming *)
     1.8  fun with_repaired_path f bnf thy =
     1.9    let
    1.10      val qualifiers =
    1.11 @@ -1324,10 +1325,10 @@
    1.12        | (_, qs, _) => qs)
    1.13    in
    1.14      thy
    1.15 -    |> Sign.root_path
    1.16 -    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
    1.17 +    (*|> Sign.root_path*)
    1.18 +    (*|> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers*)
    1.19      |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
    1.20 -    |> Sign.restore_naming thy
    1.21 +    (*|> Sign.restore_naming thy*)
    1.22    end;
    1.23  
    1.24  val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:17 2014 +0200
     2.3 @@ -193,12 +193,13 @@
     2.4    val eq: T * T -> bool = op = o pairself #T;
     2.5  );
     2.6  
     2.7 +(* FIXME naming *)
     2.8  fun with_repaired_path f (fp_sugar as {T, ...} : fp_sugar) thy =
     2.9    thy
    2.10 -  |> Sign.root_path
    2.11 -  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
    2.12 +  (*|> Sign.root_path*)
    2.13 +  (*|> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))*)
    2.14    |> (fn thy => f (morph_fp_sugar (Morphism.transfer_morphism thy) fp_sugar) thy)
    2.15 -  |> Sign.restore_naming thy;
    2.16 +  (*|> Sign.restore_naming thy*);
    2.17  
    2.18  val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
    2.19  

     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:17 2014 +0200
     3.3 @@ -158,12 +158,13 @@
     3.4    val eq: T * T -> bool = op = o pairself #ctrs;
     3.5  );
     3.6  
     3.7 +(* FIXME naming *)
     3.8  fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
     3.9    thy
    3.10 -  |> Sign.root_path
    3.11 +  (*|> Sign.root_path*)
    3.12    |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
    3.13 -  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
    3.14 -  |> Sign.restore_naming thy;
    3.15 +  (*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
    3.16 +  (*|> Sign.restore_naming thy*);
    3.17  
    3.18  val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
    3.19